Theorem: LO.System.iff_concact_disj!
Proof state before:
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! (Γ ++ Δ).disj' ⟷ Γ.disj' ⋎ Δ.disj'
Tactic:
induction Γ using List.induction_with_singleton generalizing Δ <;> induction Δ using List.induction_with_singleton
Proof state after:
case hnil.hnil
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q r : F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! ([] ++ []).disj' ⟷ [].disj' ⋎ [].disj'

case hnil.hsingle
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q r : F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
a✝ : F
⊢ 𝓢 ⊢! ([] ++ [a✝]).disj' ⟷ [].disj' ⋎ [a✝].disj'

case hnil.hcons
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q r : F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
a✝² : F
as✝ : List F
a✝¹ : as✝ ≠ []
a✝ : 𝓢 ⊢! ([] ++ as✝).disj' ⟷ [].disj' ⋎ as✝.disj'
⊢ 𝓢 ⊢! ([] ++ a✝² :: as✝).disj' ⟷ [].disj' ⋎ (a✝² :: as✝).disj'

case hsingle.hnil
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q r : F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
a✝ : F
⊢ 𝓢 ⊢! ([a✝] ++ []).disj' ⟷ [a✝].disj' ⋎ [].disj'

case hsingle.hsingle
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q r : F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
a✝¹ a✝ : F
⊢ 𝓢 ⊢! ([a✝¹] ++ [a✝]).disj' ⟷ [a✝¹].disj' ⋎ [a✝].disj'

case hsingle.hcons
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q r : F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
a✝³ a✝² : F
as✝ : List F
a✝¹ : as✝ ≠ []
a✝ : 𝓢 ⊢! ([a✝³] ++ as✝).disj' ⟷ [a✝³].disj' ⋎ as✝.disj'
⊢ 𝓢 ⊢! ([a✝³] ++ a✝² :: as✝).disj' ⟷ [a✝³].disj' ⋎ (a✝² :: as✝).disj'

case hcons.hnil
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q r : F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
a✝² : F
as✝ : List F
a✝¹ : as✝ ≠ []
a✝ : ∀ {Δ : List F}, 𝓢 ⊢! (as✝ ++ Δ).disj' ⟷ as✝.disj' ⋎ Δ.disj'
⊢ 𝓢 ⊢! (a✝² :: as✝ ++ []).disj' ⟷ (a✝² :: as✝).disj' ⋎ [].disj'

case hcons.hsingle
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q r : F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
a✝³ : F
as✝ : List F
a✝² : as✝ ≠ []
a✝¹ : ∀ {Δ : List F}, 𝓢 ⊢! (as✝ ++ Δ).disj' ⟷ as✝.disj' ⋎ Δ.disj'
a✝ : F
⊢ 𝓢 ⊢! (a✝³ :: as✝ ++ [a✝]).disj' ⟷ (a✝³ :: as✝).disj' ⋎ [a✝].disj'

case hcons.hcons
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q r : F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
a✝⁵ : F
as✝¹ : List F
a✝⁴ : as✝¹ ≠ []
a✝³ : ∀ {Δ : List F}, 𝓢 ⊢! (as✝¹ ++ Δ).disj' ⟷ as✝¹.disj' ⋎ Δ.disj'
a✝² : F
as✝ : List F
a✝¹ : as✝ ≠ []
a✝ : 𝓢 ⊢! (a✝⁵ :: as✝¹ ++ as✝).disj' ⟷ (a✝⁵ :: as✝¹).disj' ⋎ as✝.disj'
⊢ 𝓢 ⊢! (a✝⁵ :: as✝¹ ++ a✝² :: as✝).disj' ⟷ (a✝⁵ :: as✝¹).disj' ⋎ (a✝² :: as✝).disj'