Theorem: LN.lc_at_iff_lc (FOL/LN/Paper.lean)

State before:
F : Formula
⊢ Formula.lc_at 0 F ↔ F.lc
Tactic:
constructor
State after:
case mp
F : Formula
⊢ Formula.lc_at 0 F → F.lc

case mpr
F : Formula
⊢ F.lc → Formula.lc_at 0 F

State before:
case mp
F : Formula
⊢ Formula.lc_at 0 F → F.lc
Tactic:
intro a1
State after:
case mp
F : Formula
a1 : Formula.lc_at 0 F
⊢ F.lc

State before:
case mp
F : Formula
a1 : Formula.lc_at 0 F
⊢ F.lc
Tactic:
sorry
State after:
no goals

State before:
case mpr
F : Formula
⊢ F.lc → Formula.lc_at 0 F
Tactic:
intro a1
State after:
case mpr
F : Formula
a1 : F.lc
⊢ Formula.lc_at 0 F

State before:
case mpr
F : Formula
a1 : F.lc
⊢ Formula.lc_at 0 F
Tactic:
sorry
State after:
no goals