Theorem: AIG.if_as_bool (LeanSAT/AIG/If.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
d l r : Bool
⊢ (if d = true then l else r) = (d && l || !d && r)
Tactic:
revert d l r
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
⊢ ∀ (d l r : Bool), (if d = true then l else r) = (d && l || !d && r)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
⊢ ∀ (d l r : Bool), (if d = true then l else r) = (d && l || !d && r)
Tactic:
decide
State after:
no goals