Theorem: LeanSAT.Model.PropFun.var_eq_var (LeanSAT/Model/PropFun.lean)

State before:
ν : Type u_1
inst✝ : DecidableEq ν
v v' : ν
⊢ var v = var v' ↔ v = v'
Tactic:
constructor
State after:
case mp
ν : Type u_1
inst✝ : DecidableEq ν
v v' : ν
⊢ var v = var v' → v = v'

case mpr
ν : Type u_1
inst✝ : DecidableEq ν
v v' : ν
⊢ v = v' → var v = var v'

State before:
case mp
ν : Type u_1
inst✝ : DecidableEq ν
v v' : ν
⊢ var v = var v' → v = v'
Tactic:
intro
State after:
case mp
ν : Type u_1
inst✝ : DecidableEq ν
v v' : ν
a✝ : var v = var v'
⊢ v = v'

State before:
case mp
ν : Type u_1
inst✝ : DecidableEq ν
v v' : ν
a✝ : var v = var v'
⊢ v = v'
Tactic:
apply var.inj
State after:
case mp.a
ν : Type u_1
inst✝ : DecidableEq ν
v v' : ν
a✝ : var v = var v'
⊢ var v = var v'

State before:
case mp.a
ν : Type u_1
inst✝ : DecidableEq ν
v v' : ν
a✝ : var v = var v'
⊢ var v = var v'
Tactic:
assumption
State after:
no goals

State before:
case mpr
ν : Type u_1
inst✝ : DecidableEq ν
v v' : ν
⊢ v = v' → var v = var v'
Tactic:
aesop
State after:
no goals