deep-recursion.lean

namespace gapt

open tactic expr

namespace lk

lemma LogicalAxiom {a} (main1 : a) (main2 : ¬a) : false := main2 main1
lemma BottomAxiom (main : false) : false := main
lemma TopAxiom (main : ¬true) : false := main ⟨⟩
lemma ReflexivityAxiom {α : Type} {a : α} (main : a ≠ a) : false := main (eq.refl a)
lemma NegLeftRule {a} (main : ¬a) (aux : ¬¬a) : false := aux main
lemma NegRightRule {a} (main : ¬¬a) (aux : ¬a) : false := main aux
lemma AndLeftRule {a b} (main : a ∧ b) (aux : a → b → false) : false :=
aux main^.left main^.right
lemma AndRightRule {a b} (main : ¬(a ∧ b)) (aux1 : ¬¬a) (aux2 : ¬¬b) : false :=
aux1 $ λa, aux2 $ λb, main ⟨a,b⟩
lemma OrLeftRule {a b} (main : a ∨ b) (aux1 : ¬a) (aux2 : ¬b) : false :=
begin cases main, contradiction, contradiction end
lemma OrRightRule {a b} (main : ¬(a ∨ b)) (aux : ¬a → ¬b → false) : false :=
aux (main ∘ or.inl) (main ∘ or.inr)
lemma ImpLeftRule {a b} (main : a → b) (aux1 : ¬¬a) (aux2 : ¬b) : false := aux1 (aux2 ∘ main)
lemma ImpRightRule {a b : Prop} (main : ¬(a → b)) (aux : a → ¬b → false) : false :=
main (classical.by_contradiction ∘ aux)
lemma ForallLeftRule {α} {P : α → Prop} (t) (main : ∀x, P x) (aux : ¬P t) : false := aux (main t)
lemma ForallRightRule {α} {P : α → Prop} (main : ¬∀x, P x) (aux : Πx, ¬P x → false) : false :=
begin apply main, intro x, apply classical.by_contradiction, intro, apply aux, assumption end
lemma ExistsLeftRule {α} {P : α → Prop} (main : ∃x, P x) (aux : Πx, P x → false) : false :=
begin cases main, apply aux, assumption end
lemma ExistsRightRule {α} {P : α → Prop} (t) (main : ¬∃x, P x) (aux : ¬¬P t) : false :=
begin apply aux, intro hp, apply main, existsi t, assumption end
lemma EqualityLeftRule1 {α} (c : α → Prop) (t s) (main1 : t=s) (main2 : c s) (aux : ¬c t) : false :=
begin apply aux, rw main1, assumption end
lemma EqualityRightRule1 {α} (c : α → Prop) (t s) (main1 : t=s) (main2 : ¬c s) (aux : ¬¬c t) : false :=
begin apply aux, rw main1, assumption end
lemma EqualityLeftRule2 {α} (c : α → Prop) (t s) (main1 : s=t) (main2 : c s) (aux : ¬c t) : false :=
EqualityLeftRule1 c t s main1^.symm main2 aux
lemma EqualityRightRule2 {α} (c : α → Prop) (t s) (main1 : s=t) (main2 : ¬c s) (aux : ¬¬c t) : false :=
EqualityRightRule1 c t s main1^.symm main2 aux
lemma CutRule (a : Prop) (aux1 : ¬¬a) (aux2 : ¬a) : false := aux1 aux2

lemma unpack_target_disj.cons {a b} (next : ¬a → b) : a ∨ b :=
classical.by_cases or.inl (or.inr ∘ next)
lemma unpack_target_disj.singleton {a} : ¬¬a → a := classical.by_contradiction
private meta def unpack_target_disj : list name → command
| [] := skip
| [h] := do tgt ← target,
            apply $ app (const ``gapt.lk.unpack_target_disj.singleton []) tgt,
            intro h, skip
| (h::hs) := do tgt ← target,
                a ← return $ tgt^.app_fn^.app_arg,
                b ← return $ tgt^.app_arg,
                apply $ app_of_list (const ``gapt.lk.unpack_target_disj.cons []) [a, b],
                intro h,
                unpack_target_disj hs

meta def sequent_formula_to_hyps (ant suc : list name) : command := do
intro_lst ant, unpack_target_disj suc

end lk

end gapt

noncomputable theory

namespace gapt_export

def all {a : Type} (P : a -> Prop) := ∀x, P x

constant i : Type

constant cap : (i -> (i -> i))

constant cup : (i -> (i -> i))

axiom ax : (∀ x : i, (∀ y : i, ((cap x y) = (cap y x))))

axiom ax_0 : (∀ x : i, (∀ y : i, (∀ z : i, ((cap (cap x y) z) = (cap x (cap y z))))))

axiom ax_1 : (∀ x : i, ((cap x x) = x))

axiom ax_2 : (∀ x : i, (∀ y : i, ((cup x y) = (cup y x))))

axiom ax_3 : (∀ x : i, (∀ y : i, (∀ z : i, ((cup (cup x y) z) = (cup x (cup y z))))))

axiom ax_4 : (∀ x : i, ((cup x x) = x))

def lt_eq : (i -> (i -> Prop)) := (λ x : i, (λ y : i, ((cap x y) = x)))

def L1 : Prop := (∀ x : i, (∀ y : i, (and (((cap x y) = x) -> ((cup x y) = y)) (((cup x y) = y) -> ((cap x y) = x)))))

def L2 : Prop := (and (∀ x : i, (∀ y : i, ((cup (cap x y) x) = x))) (∀ x : i, (∀ y : i, ((cap (cup x y) x) = x))))

def R : Prop := (∀ x : i, (lt_eq x x))

def AS : Prop := (∀ x : i, (∀ y : i, ((and (lt_eq x y) (lt_eq y x)) -> (x = y))))

def T : Prop := (∀ x : i, (∀ y : i, (∀ z : i, ((and (lt_eq x y) (lt_eq y z)) -> (lt_eq x z)))))

def POSET : Prop := (and R (and AS T))

def GLB : Prop := (∀ x : i, (∀ y : i, (and (and (lt_eq (cap x y) x) (lt_eq (cap x y) y)) (∀ z : i, ((and (lt_eq z x) (lt_eq z y)) -> (lt_eq z (cap x y)))))))

def LUB : Prop := (∀ x : i, (∀ y : i, (and (and (lt_eq x (cup x y)) (lt_eq y (cup x y))) (∀ z : i, ((and (lt_eq x z) (lt_eq y z)) -> (lt_eq (cup x y) z))))))

def L3 : Prop := (and POSET (and GLB LUB))

lemma lk_proof : (L1 -> L2) :=
begin
tactic.failed,
gapt.lk.sequent_formula_to_hyps [`hyp.h_0] [`hyp.h_1],
apply (gapt.lk.CutRule L3), intros hyp.h_2,
apply (gapt.lk.AndRightRule hyp.h_2), intros hyp.h_3,
apply (gapt.lk.AndRightRule hyp.h_3), intros hyp.h_4,
apply (gapt.lk.ForallRightRule hyp.h_4), intros x hyp.h_5,
apply (gapt.lk.CutRule (x = x)), intros hyp.h_6,
apply (gapt.lk.ReflexivityAxiom hyp.h_6), intros hyp.h_6,
apply (gapt.lk.CutRule (x = (cap x x))), intros hyp.h_7,
apply (gapt.lk.CutRule ((cap x x) = x)), intros hyp.h_8,
exact sorry,
intros hyp.h_8,
apply (gapt.lk.EqualityRightRule1 (λ x_0 : i, (x_0 = (cap x x))) (cap x x) x hyp.h_8 hyp.h_7), intros hyp.h_9,
apply (gapt.lk.ReflexivityAxiom hyp.h_9), intros hyp.h_7,
apply (gapt.lk.EqualityLeftRule2 (λ x_1 : i, (x = x_1)) (cap x x) x hyp.h_7 hyp.h_6), intros hyp.h_8,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, (x_1 = x)) x (cap x x) hyp.h_8 hyp.h_5), intros hyp.h_9,
apply (gapt.lk.ReflexivityAxiom hyp.h_9), intros hyp.h_4,
apply (gapt.lk.AndRightRule hyp.h_4), intros hyp.h_5,
apply (gapt.lk.ForallRightRule hyp.h_5), intros x hyp.h_6,
apply (gapt.lk.ForallRightRule hyp.h_6), intros y hyp.h_7,
apply (gapt.lk.ImpRightRule hyp.h_7), intros hyp.h_8 hyp.h_9,
apply (gapt.lk.AndLeftRule hyp.h_8), intros hyp.h_10 hyp.h_11,
apply (gapt.lk.CutRule (x = x)), intros hyp.h_12,
apply (gapt.lk.ReflexivityAxiom hyp.h_12), intros hyp.h_12,
apply (gapt.lk.CutRule (x = y)), intros hyp.h_13,
apply (gapt.lk.CutRule (y = x)), intros hyp.h_14,
apply (gapt.lk.CutRule (x = (cap x y))), intros hyp.h_15,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, (x_1 = (cap x y))) (cap x y) x hyp.h_10 hyp.h_15), intros hyp.h_16,
apply (gapt.lk.ReflexivityAxiom hyp.h_16), intros hyp.h_15,
apply (gapt.lk.EqualityRightRule2 (λ x_1 : i, (y = x_1)) (cap x y) x hyp.h_15 hyp.h_14), intros hyp.h_16,
apply (gapt.lk.CutRule ((cap y x) = (cap x y))), intros hyp.h_17,
exact sorry,
intros hyp.h_17,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, (y = x_1)) (cap y x) (cap x y) hyp.h_17 hyp.h_16), intros hyp.h_18,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, (x_1 = (cap y x))) (cap y x) y hyp.h_11 hyp.h_18), intros hyp.h_19,
apply (gapt.lk.ReflexivityAxiom hyp.h_19), intros hyp.h_14,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, (x_1 = y)) y x hyp.h_14 hyp.h_13), intros hyp.h_15,
apply (gapt.lk.ReflexivityAxiom hyp.h_15), intros hyp.h_13,
apply (gapt.lk.EqualityLeftRule2 (λ x_1 : i, (x = x_1)) y x hyp.h_13 hyp.h_12), intros hyp.h_14,
apply (gapt.lk.LogicalAxiom hyp.h_14 hyp.h_9), intros hyp.h_5,
apply (gapt.lk.ForallRightRule hyp.h_5), intros x hyp.h_6,
apply (gapt.lk.ForallRightRule hyp.h_6), intros y hyp.h_7,
apply (gapt.lk.ForallRightRule hyp.h_7), intros z hyp.h_8,
apply (gapt.lk.ImpRightRule hyp.h_8), intros hyp.h_9 hyp.h_10,
apply (gapt.lk.AndLeftRule hyp.h_9), intros hyp.h_11 hyp.h_12,
apply (gapt.lk.CutRule (x = x)), intros hyp.h_13,
apply (gapt.lk.ReflexivityAxiom hyp.h_13), intros hyp.h_13,
apply (gapt.lk.CutRule (x = (cap x z))), intros hyp.h_14,
apply (gapt.lk.CutRule ((cap x z) = x)), intros hyp.h_15,
apply (gapt.lk.CutRule (x = (cap x y))), intros hyp.h_16,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, (x_1 = (cap x y))) (cap x y) x hyp.h_11 hyp.h_16), intros hyp.h_17,
apply (gapt.lk.ReflexivityAxiom hyp.h_17), intros hyp.h_16,
apply (gapt.lk.EqualityRightRule2 (λ x_1 : i, ((cap x z) = x_1)) (cap x y) x hyp.h_16 hyp.h_15), intros hyp.h_17,
apply (gapt.lk.CutRule (y = (cap z y))), intros hyp.h_18,
apply (gapt.lk.CutRule ((cap y z) = (cap z y))), intros hyp.h_19,
exact sorry,
intros hyp.h_19,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, (y = x_1)) (cap y z) (cap z y) hyp.h_19 hyp.h_18), intros hyp.h_20,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, (x_1 = (cap y z))) (cap y z) y hyp.h_12 hyp.h_20), intros hyp.h_21,
apply (gapt.lk.ReflexivityAxiom hyp.h_21), intros hyp.h_18,
apply (gapt.lk.EqualityRightRule2 (λ x_1 : i, ((cap x z) = (cap x x_1))) (cap z y) y hyp.h_18 hyp.h_17), intros hyp.h_19,
apply (gapt.lk.CutRule ((cap y z) = (cap z y))), intros hyp.h_20,
exact sorry,
intros hyp.h_20,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, ((cap x z) = (cap x x_1))) (cap y z) (cap z y) hyp.h_20 hyp.h_19), intros hyp.h_21,
apply (gapt.lk.CutRule ((cap x (cap y z)) = (cap x z))), intros hyp.h_22,
apply (gapt.lk.CutRule (x = (cap x y))), intros hyp.h_23,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, (x_1 = (cap x y))) (cap x y) x hyp.h_11 hyp.h_23), intros hyp.h_24,
apply (gapt.lk.ReflexivityAxiom hyp.h_24), intros hyp.h_23,
apply (gapt.lk.EqualityRightRule2 (λ x_1 : i, ((cap x (cap y z)) = (cap x_1 z))) (cap x y) x hyp.h_23 hyp.h_22), intros hyp.h_24,
apply (gapt.lk.CutRule ((cap (cap x y) z) = (cap x (cap y z)))), intros hyp.h_25,
exact sorry,
intros hyp.h_25,
apply (gapt.lk.EqualityRightRule1 (λ x_0 : i, (x_0 = (cap (cap x y) z))) (cap (cap x y) z) (cap x (cap y z)) hyp.h_25 hyp.h_24), intros hyp.h_26,
apply (gapt.lk.ReflexivityAxiom hyp.h_26), intros hyp.h_22,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, (x_1 = (cap x (cap y z)))) (cap x (cap y z)) (cap x z) hyp.h_22 hyp.h_21), intros hyp.h_23,
apply (gapt.lk.ReflexivityAxiom hyp.h_23), intros hyp.h_15,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, (x_1 = (cap x z))) (cap x z) x hyp.h_15 hyp.h_14), intros hyp.h_16,
apply (gapt.lk.ReflexivityAxiom hyp.h_16), intros hyp.h_14,
apply (gapt.lk.EqualityLeftRule2 (λ x_1 : i, (x = x_1)) (cap x z) x hyp.h_14 hyp.h_13), intros hyp.h_15,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, (x_1 = x)) x (cap x z) hyp.h_15 hyp.h_10), intros hyp.h_16,
apply (gapt.lk.ReflexivityAxiom hyp.h_16), intros hyp.h_3,
apply (gapt.lk.AndRightRule hyp.h_3), intros hyp.h_4,
apply (gapt.lk.ForallRightRule hyp.h_4), intros x hyp.h_5,
apply (gapt.lk.ForallRightRule hyp.h_5), intros y hyp.h_6,
apply (gapt.lk.AndRightRule hyp.h_6), intros hyp.h_7,
apply (gapt.lk.AndRightRule hyp.h_7), intros hyp.h_8,
apply (gapt.lk.CutRule ((cap x y) = (cap x y))), intros hyp.h_9,
apply (gapt.lk.ReflexivityAxiom hyp.h_9), intros hyp.h_9,
apply (gapt.lk.CutRule ((cap x y) = (cap x (cap x y)))), intros hyp.h_10,
apply (gapt.lk.CutRule ((cap x (cap x y)) = (cap x y))), intros hyp.h_11,
apply (gapt.lk.CutRule (x = (cap x x))), intros hyp.h_12,
apply (gapt.lk.CutRule ((cap x x) = x)), intros hyp.h_13,
exact sorry,
intros hyp.h_13,
apply (gapt.lk.EqualityRightRule1 (λ x_0 : i, (x_0 = (cap x x))) (cap x x) x hyp.h_13 hyp.h_12), intros hyp.h_14,
apply (gapt.lk.ReflexivityAxiom hyp.h_14), intros hyp.h_12,
apply (gapt.lk.EqualityRightRule2 (λ x_2 : i, ((cap x (cap x y)) = (cap x_2 y))) (cap x x) x hyp.h_12 hyp.h_11), intros hyp.h_13,
apply (gapt.lk.CutRule ((cap (cap x x) y) = (cap x (cap x y)))), intros hyp.h_14,
exact sorry,
intros hyp.h_14,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, (x_1 = (cap (cap x x) y))) (cap (cap x x) y) (cap x (cap x y)) hyp.h_14 hyp.h_13), intros hyp.h_15,
apply (gapt.lk.ReflexivityAxiom hyp.h_15), intros hyp.h_11,
apply (gapt.lk.EqualityRightRule1 (λ x_2 : i, (x_2 = (cap x (cap x y)))) (cap x (cap x y)) (cap x y) hyp.h_11 hyp.h_10), intros hyp.h_12,
apply (gapt.lk.ReflexivityAxiom hyp.h_12), intros hyp.h_10,
apply (gapt.lk.EqualityLeftRule2 (λ x_2 : i, ((cap x y) = x_2)) (cap x (cap x y)) (cap x y) hyp.h_10 hyp.h_9), intros hyp.h_11,
apply (gapt.lk.CutRule ((cap x y) = (cap y x))), intros hyp.h_12,
exact sorry,
intros hyp.h_12,
apply (gapt.lk.EqualityLeftRule2 (λ x_2 : i, ((cap x y) = (cap x x_2))) (cap y x) (cap x y) hyp.h_12 hyp.h_11), intros hyp.h_13,
apply (gapt.lk.CutRule ((cap x (cap y x)) = (cap (cap x y) x))), intros hyp.h_14,
apply (gapt.lk.CutRule ((cap (cap x y) x) = (cap x (cap y x)))), intros hyp.h_15,
exact sorry,
intros hyp.h_15,
apply (gapt.lk.EqualityRightRule1 (λ x_0 : i, (x_0 = (cap (cap x y) x))) (cap (cap x y) x) (cap x (cap y x)) hyp.h_15 hyp.h_14), intros hyp.h_16,
apply (gapt.lk.ReflexivityAxiom hyp.h_16), intros hyp.h_14,
apply (gapt.lk.EqualityLeftRule2 (λ x_2 : i, ((cap x y) = x_2)) (cap (cap x y) x) (cap x (cap y x)) hyp.h_14 hyp.h_13), intros hyp.h_15,
apply (gapt.lk.EqualityRightRule1 (λ x_2 : i, (x_2 = (cap x y))) (cap x y) (cap (cap x y) x) hyp.h_15 hyp.h_8), intros hyp.h_16,
apply (gapt.lk.ReflexivityAxiom hyp.h_16), intros hyp.h_8,
apply (gapt.lk.CutRule ((cap x y) = (cap x y))), intros hyp.h_9,
apply (gapt.lk.ReflexivityAxiom hyp.h_9), intros hyp.h_9,
apply (gapt.lk.CutRule ((cap x y) = (cap y x))), intros hyp.h_10,
exact sorry,
intros hyp.h_10,
apply (gapt.lk.EqualityLeftRule2 (λ x_1 : i, ((cap x y) = x_1)) (cap y x) (cap x y) hyp.h_10 hyp.h_9), intros hyp.h_11,
apply (gapt.lk.CutRule ((cap y x) = (cap y (cap x y)))), intros hyp.h_12,
apply (gapt.lk.CutRule ((cap y x) = (cap x y))), intros hyp.h_13,
exact sorry,
intros hyp.h_13,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, ((cap y x) = (cap y x_1))) (cap y x) (cap x y) hyp.h_13 hyp.h_12), intros hyp.h_14,
apply (gapt.lk.CutRule ((cap y (cap y x)) = (cap y x))), intros hyp.h_15,
apply (gapt.lk.CutRule (y = (cap y y))), intros hyp.h_16,
apply (gapt.lk.CutRule ((cap y y) = y)), intros hyp.h_17,
exact sorry,
intros hyp.h_17,
apply (gapt.lk.EqualityRightRule1 (λ x_2 : i, (x_2 = (cap y y))) (cap y y) y hyp.h_17 hyp.h_16), intros hyp.h_18,
apply (gapt.lk.ReflexivityAxiom hyp.h_18), intros hyp.h_16,
apply (gapt.lk.EqualityRightRule2 (λ x_1 : i, ((cap y (cap y x)) = (cap x_1 x))) (cap y y) y hyp.h_16 hyp.h_15), intros hyp.h_17,
apply (gapt.lk.CutRule ((cap (cap y y) x) = (cap y (cap y x)))), intros hyp.h_18,
exact sorry,
intros hyp.h_18,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, (x_1 = (cap (cap y y) x))) (cap (cap y y) x) (cap y (cap y x)) hyp.h_18 hyp.h_17), intros hyp.h_19,
apply (gapt.lk.ReflexivityAxiom hyp.h_19), intros hyp.h_15,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, (x_1 = (cap y (cap y x)))) (cap y (cap y x)) (cap y x) hyp.h_15 hyp.h_14), intros hyp.h_16,
apply (gapt.lk.ReflexivityAxiom hyp.h_16), intros hyp.h_12,
apply (gapt.lk.EqualityLeftRule2 (λ x_1 : i, ((cap x y) = x_1)) (cap y (cap x y)) (cap y x) hyp.h_12 hyp.h_11), intros hyp.h_13,
apply (gapt.lk.CutRule ((cap (cap x y) y) = (cap y (cap x y)))), intros hyp.h_14,
exact sorry,
intros hyp.h_14,
apply (gapt.lk.EqualityLeftRule1 (λ x_1 : i, ((cap x y) = x_1)) (cap (cap x y) y) (cap y (cap x y)) hyp.h_14 hyp.h_13), intros hyp.h_15,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, (x_1 = (cap x y))) (cap x y) (cap (cap x y) y) hyp.h_15 hyp.h_8), intros hyp.h_16,
apply (gapt.lk.ReflexivityAxiom hyp.h_16), intros hyp.h_7,
apply (gapt.lk.ForallRightRule hyp.h_7), intros z hyp.h_8,
apply (gapt.lk.ImpRightRule hyp.h_8), intros hyp.h_9 hyp.h_10,
apply (gapt.lk.AndLeftRule hyp.h_9), intros hyp.h_11 hyp.h_12,
apply (gapt.lk.CutRule (z = z)), intros hyp.h_13,
apply (gapt.lk.ReflexivityAxiom hyp.h_13), intros hyp.h_13,
apply (gapt.lk.CutRule (z = (cap y z))), intros hyp.h_14,
apply (gapt.lk.CutRule ((cap z y) = (cap y z))), intros hyp.h_15,
exact sorry,
intros hyp.h_15,
apply (gapt.lk.EqualityRightRule1 (λ x_0 : i, (z = x_0)) (cap z y) (cap y z) hyp.h_15 hyp.h_14), intros hyp.h_16,
apply (gapt.lk.EqualityRightRule1 (λ x_0 : i, (x_0 = (cap z y))) (cap z y) z hyp.h_12 hyp.h_16), intros hyp.h_17,
apply (gapt.lk.ReflexivityAxiom hyp.h_17), intros hyp.h_14,
apply (gapt.lk.EqualityLeftRule2 (λ x_0 : i, (z = x_0)) (cap y z) z hyp.h_14 hyp.h_13), intros hyp.h_15,
apply (gapt.lk.CutRule ((cap y z) = (cap z y))), intros hyp.h_16,
exact sorry,
intros hyp.h_16,
apply (gapt.lk.EqualityLeftRule2 (λ x_0 : i, (z = x_0)) (cap z y) (cap y z) hyp.h_16 hyp.h_15), intros hyp.h_17,
apply (gapt.lk.CutRule ((cap z y) = (cap z (cap x y)))), intros hyp.h_18,
apply (gapt.lk.CutRule ((cap z (cap x y)) = (cap z y))), intros hyp.h_19,
apply (gapt.lk.CutRule (z = (cap z x))), intros hyp.h_20,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, (x_1 = (cap z x))) (cap z x) z hyp.h_11 hyp.h_20), intros hyp.h_21,
apply (gapt.lk.ReflexivityAxiom hyp.h_21), intros hyp.h_20,
apply (gapt.lk.EqualityRightRule2 (λ x_1 : i, ((cap z (cap x y)) = (cap x_1 y))) (cap z x) z hyp.h_20 hyp.h_19), intros hyp.h_21,
apply (gapt.lk.CutRule ((cap (cap z x) y) = (cap z (cap x y)))), intros hyp.h_22,
exact sorry,
intros hyp.h_22,
apply (gapt.lk.EqualityRightRule1 (λ x_2 : i, (x_2 = (cap (cap z x) y))) (cap (cap z x) y) (cap z (cap x y)) hyp.h_22 hyp.h_21), intros hyp.h_23,
apply (gapt.lk.ReflexivityAxiom hyp.h_23), intros hyp.h_19,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, (x_1 = (cap z (cap x y)))) (cap z (cap x y)) (cap z y) hyp.h_19 hyp.h_18), intros hyp.h_20,
apply (gapt.lk.ReflexivityAxiom hyp.h_20), intros hyp.h_18,
apply (gapt.lk.EqualityLeftRule2 (λ x_0 : i, (z = x_0)) (cap z (cap x y)) (cap z y) hyp.h_18 hyp.h_17), intros hyp.h_19,
apply (gapt.lk.EqualityRightRule1 (λ x_0 : i, (x_0 = z)) z (cap z (cap x y)) hyp.h_19 hyp.h_10), intros hyp.h_20,
apply (gapt.lk.ReflexivityAxiom hyp.h_20), intros hyp.h_4,
apply (gapt.lk.ForallRightRule hyp.h_4), intros x_0 hyp.h_5,
apply (gapt.lk.ForallRightRule hyp.h_5), intros y_0 hyp.h_6,
apply (gapt.lk.AndRightRule hyp.h_6), intros hyp.h_7,
apply (gapt.lk.AndRightRule hyp.h_7), intros hyp.h_8,
apply (gapt.lk.ForallLeftRule x_0 hyp.h_0), intros hyp.h_9,
apply (gapt.lk.ForallLeftRule (cup x_0 y_0) hyp.h_9), intros hyp.h_10,
apply (gapt.lk.AndLeftRule hyp.h_10), intros hyp.h_11 hyp.h_12,
apply (gapt.lk.ImpLeftRule hyp.h_12), intros hyp.h_13,
apply (gapt.lk.CutRule ((cup x_0 y_0) = (cup x_0 y_0))), intros hyp.h_14,
apply (gapt.lk.ReflexivityAxiom hyp.h_14), intros hyp.h_14,
apply (gapt.lk.CutRule ((cup x_0 y_0) = (cup x_0 (cup x_0 y_0)))), intros hyp.h_15,
apply (gapt.lk.CutRule ((cup x_0 (cup x_0 y_0)) = (cup x_0 y_0))), intros hyp.h_16,
apply (gapt.lk.CutRule (x_0 = (cup x_0 x_0))), intros hyp.h_17,
apply (gapt.lk.CutRule ((cup x_0 x_0) = x_0)), intros hyp.h_18,
exact sorry,
intros hyp.h_18,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, (x_1 = (cup x_0 x_0))) (cup x_0 x_0) x_0 hyp.h_18 hyp.h_17), intros hyp.h_19,
apply (gapt.lk.ReflexivityAxiom hyp.h_19), intros hyp.h_17,
apply (gapt.lk.EqualityRightRule2 (λ x_2 : i, ((cup x_0 (cup x_0 y_0)) = (cup x_2 y_0))) (cup x_0 x_0) x_0 hyp.h_17 hyp.h_16), intros hyp.h_18,
apply (gapt.lk.CutRule ((cup (cup x_0 x_0) y_0) = (cup x_0 (cup x_0 y_0)))), intros hyp.h_19,
exact sorry,
intros hyp.h_19,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, (x_1 = (cup (cup x_0 x_0) y_0))) (cup (cup x_0 x_0) y_0) (cup x_0 (cup x_0 y_0)) hyp.h_19 hyp.h_18), intros hyp.h_20,
apply (gapt.lk.ReflexivityAxiom hyp.h_20), intros hyp.h_16,
apply (gapt.lk.EqualityRightRule1 (λ x_2 : i, (x_2 = (cup x_0 (cup x_0 y_0)))) (cup x_0 (cup x_0 y_0)) (cup x_0 y_0) hyp.h_16 hyp.h_15), intros hyp.h_17,
apply (gapt.lk.ReflexivityAxiom hyp.h_17), intros hyp.h_15,
apply (gapt.lk.EqualityLeftRule2 (λ x_2 : i, ((cup x_0 y_0) = x_2)) (cup x_0 (cup x_0 y_0)) (cup x_0 y_0) hyp.h_15 hyp.h_14), intros hyp.h_16,
apply (gapt.lk.EqualityRightRule1 (λ x_2 : i, (x_2 = (cup x_0 y_0))) (cup x_0 y_0) (cup x_0 (cup x_0 y_0)) hyp.h_16 hyp.h_13), intros hyp.h_17,
apply (gapt.lk.ReflexivityAxiom hyp.h_17), intros hyp.h_13,
apply (gapt.lk.LogicalAxiom hyp.h_13 hyp.h_8), intros hyp.h_8,
apply (gapt.lk.CutRule ((cup x_0 y_0) = (cup y_0 x_0))), intros hyp.h_9,
apply (gapt.lk.CutRule ((cup x_0 y_0) = (cup x_0 y_0))), intros hyp.h_10,
apply (gapt.lk.ReflexivityAxiom hyp.h_10), intros hyp.h_10,
apply (gapt.lk.CutRule ((cup y_0 x_0) = (cup x_0 y_0))), intros hyp.h_11,
exact sorry,
intros hyp.h_11,
apply (gapt.lk.EqualityLeftRule1 (λ x : i, ((cup x_0 y_0) = x)) (cup y_0 x_0) (cup x_0 y_0) hyp.h_11 hyp.h_10), intros hyp.h_12,
apply (gapt.lk.LogicalAxiom hyp.h_12 hyp.h_9), intros hyp.h_9,
apply (gapt.lk.EqualityRightRule2 (λ x : i, (lt_eq y_0 x)) (cup y_0 x_0) (cup x_0 y_0) hyp.h_9 hyp.h_8), intros hyp.h_10,
apply (gapt.lk.ForallLeftRule y_0 hyp.h_0), intros hyp.h_11,
apply (gapt.lk.ForallLeftRule (cup y_0 x_0) hyp.h_11), intros hyp.h_12,
apply (gapt.lk.AndLeftRule hyp.h_12), intros hyp.h_13 hyp.h_14,
apply (gapt.lk.ImpLeftRule hyp.h_14), intros hyp.h_15,
apply (gapt.lk.CutRule ((cup y_0 x_0) = (cup y_0 x_0))), intros hyp.h_16,
apply (gapt.lk.ReflexivityAxiom hyp.h_16), intros hyp.h_16,
apply (gapt.lk.CutRule ((cup y_0 x_0) = (cup y_0 (cup y_0 x_0)))), intros hyp.h_17,
apply (gapt.lk.CutRule ((cup y_0 (cup y_0 x_0)) = (cup y_0 x_0))), intros hyp.h_18,
apply (gapt.lk.CutRule (y_0 = (cup y_0 y_0))), intros hyp.h_19,
apply (gapt.lk.CutRule ((cup y_0 y_0) = y_0)), intros hyp.h_20,
exact sorry,
intros hyp.h_20,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, (x_1 = (cup y_0 y_0))) (cup y_0 y_0) y_0 hyp.h_20 hyp.h_19), intros hyp.h_21,
apply (gapt.lk.ReflexivityAxiom hyp.h_21), intros hyp.h_19,
apply (gapt.lk.EqualityRightRule2 (λ x_2 : i, ((cup y_0 (cup y_0 x_0)) = (cup x_2 x_0))) (cup y_0 y_0) y_0 hyp.h_19 hyp.h_18), intros hyp.h_20,
apply (gapt.lk.CutRule ((cup (cup y_0 y_0) x_0) = (cup y_0 (cup y_0 x_0)))), intros hyp.h_21,
exact sorry,
intros hyp.h_21,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, (x_1 = (cup (cup y_0 y_0) x_0))) (cup (cup y_0 y_0) x_0) (cup y_0 (cup y_0 x_0)) hyp.h_21 hyp.h_20), intros hyp.h_22,
apply (gapt.lk.ReflexivityAxiom hyp.h_22), intros hyp.h_18,
apply (gapt.lk.EqualityRightRule1 (λ x_2 : i, (x_2 = (cup y_0 (cup y_0 x_0)))) (cup y_0 (cup y_0 x_0)) (cup y_0 x_0) hyp.h_18 hyp.h_17), intros hyp.h_19,
apply (gapt.lk.ReflexivityAxiom hyp.h_19), intros hyp.h_17,
apply (gapt.lk.EqualityLeftRule2 (λ x_2 : i, ((cup y_0 x_0) = x_2)) (cup y_0 (cup y_0 x_0)) (cup y_0 x_0) hyp.h_17 hyp.h_16), intros hyp.h_18,
apply (gapt.lk.EqualityRightRule1 (λ x_2 : i, (x_2 = (cup y_0 x_0))) (cup y_0 x_0) (cup y_0 (cup y_0 x_0)) hyp.h_18 hyp.h_15), intros hyp.h_19,
apply (gapt.lk.ReflexivityAxiom hyp.h_19), intros hyp.h_15,
apply (gapt.lk.LogicalAxiom hyp.h_15 hyp.h_10), intros hyp.h_7,
apply (gapt.lk.ForallRightRule hyp.h_7), intros z_0 hyp.h_8,
apply (gapt.lk.ImpRightRule hyp.h_8), intros hyp.h_9 hyp.h_10,
apply (gapt.lk.AndLeftRule hyp.h_9), intros hyp.h_11 hyp.h_12,
apply (gapt.lk.ForallLeftRule x_0 hyp.h_0), intros hyp.h_13,
apply (gapt.lk.ForallLeftRule z_0 hyp.h_13), intros hyp.h_14,
apply (gapt.lk.AndLeftRule hyp.h_14), intros hyp.h_15 hyp.h_16,
apply (gapt.lk.ImpLeftRule hyp.h_15), intros hyp.h_16,
apply (gapt.lk.LogicalAxiom hyp.h_11 hyp.h_16), intros hyp.h_16,
apply (gapt.lk.ForallLeftRule y_0 hyp.h_0), intros hyp.h_17,
apply (gapt.lk.ForallLeftRule z_0 hyp.h_17), intros hyp.h_18,
apply (gapt.lk.AndLeftRule hyp.h_18), intros hyp.h_19 hyp.h_20,
apply (gapt.lk.ImpLeftRule hyp.h_19), intros hyp.h_20,
apply (gapt.lk.LogicalAxiom hyp.h_12 hyp.h_20), intros hyp.h_20,
apply (gapt.lk.ForallLeftRule (cup x_0 y_0) hyp.h_0), intros hyp.h_21,
apply (gapt.lk.ForallLeftRule z_0 hyp.h_21), intros hyp.h_22,
apply (gapt.lk.AndLeftRule hyp.h_22), intros hyp.h_23 hyp.h_24,
apply (gapt.lk.ImpLeftRule hyp.h_24), intros hyp.h_25,
apply (gapt.lk.CutRule (z_0 = z_0)), intros hyp.h_26,
apply (gapt.lk.ReflexivityAxiom hyp.h_26), intros hyp.h_26,
apply (gapt.lk.CutRule (z_0 = (cup x_0 z_0))), intros hyp.h_27,
apply (gapt.lk.EqualityRightRule1 (λ x : i, (x = (cup x_0 z_0))) (cup x_0 z_0) z_0 hyp.h_16 hyp.h_27), intros hyp.h_28,
apply (gapt.lk.ReflexivityAxiom hyp.h_28), intros hyp.h_27,
apply (gapt.lk.EqualityLeftRule2 (λ x : i, (z_0 = x)) (cup x_0 z_0) z_0 hyp.h_27 hyp.h_26), intros hyp.h_28,
apply (gapt.lk.CutRule ((cup x_0 z_0) = (cup z_0 x_0))), intros hyp.h_29,
exact sorry,
intros hyp.h_29,
apply (gapt.lk.EqualityLeftRule2 (λ x : i, (z_0 = x)) (cup z_0 x_0) (cup x_0 z_0) hyp.h_29 hyp.h_28), intros hyp.h_30,
apply (gapt.lk.CutRule ((cup z_0 x_0) = (cup z_0 (cup x_0 y_0)))), intros hyp.h_31,
apply (gapt.lk.CutRule ((cup z_0 (cup x_0 y_0)) = (cup z_0 x_0))), intros hyp.h_32,
apply (gapt.lk.CutRule ((cup z_0 x_0) = (cup z_0 (cup x_0 z_0)))), intros hyp.h_33,
apply (gapt.lk.CutRule ((cup x_0 z_0) = (cup z_0 x_0))), intros hyp.h_34,
exact sorry,
intros hyp.h_34,
apply (gapt.lk.EqualityRightRule2 (λ x : i, ((cup z_0 x_0) = (cup z_0 x))) (cup z_0 x_0) (cup x_0 z_0) hyp.h_34 hyp.h_33), intros hyp.h_35,
apply (gapt.lk.CutRule ((cup z_0 (cup z_0 x_0)) = (cup z_0 x_0))), intros hyp.h_36,
apply (gapt.lk.CutRule (z_0 = (cup z_0 z_0))), intros hyp.h_37,
apply (gapt.lk.CutRule ((cup z_0 z_0) = z_0)), intros hyp.h_38,
exact sorry,
intros hyp.h_38,
apply (gapt.lk.EqualityRightRule1 (λ x_2 : i, (x_2 = (cup z_0 z_0))) (cup z_0 z_0) z_0 hyp.h_38 hyp.h_37), intros hyp.h_39,
apply (gapt.lk.ReflexivityAxiom hyp.h_39), intros hyp.h_37,
apply (gapt.lk.EqualityRightRule2 (λ x : i, ((cup z_0 (cup z_0 x_0)) = (cup x x_0))) (cup z_0 z_0) z_0 hyp.h_37 hyp.h_36), intros hyp.h_38,
apply (gapt.lk.CutRule ((cup (cup z_0 z_0) x_0) = (cup z_0 (cup z_0 x_0)))), intros hyp.h_39,
exact sorry,
intros hyp.h_39,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, (x_1 = (cup (cup z_0 z_0) x_0))) (cup (cup z_0 z_0) x_0) (cup z_0 (cup z_0 x_0)) hyp.h_39 hyp.h_38), intros hyp.h_40,
apply (gapt.lk.ReflexivityAxiom hyp.h_40), intros hyp.h_36,
apply (gapt.lk.EqualityRightRule1 (λ x : i, (x = (cup z_0 (cup z_0 x_0)))) (cup z_0 (cup z_0 x_0)) (cup z_0 x_0) hyp.h_36 hyp.h_35), intros hyp.h_37,
apply (gapt.lk.ReflexivityAxiom hyp.h_37), intros hyp.h_33,
apply (gapt.lk.EqualityRightRule2 (λ x : i, ((cup z_0 (cup x_0 y_0)) = x)) (cup z_0 (cup x_0 z_0)) (cup z_0 x_0) hyp.h_33 hyp.h_32), intros hyp.h_34,
apply (gapt.lk.CutRule ((cup x_0 z_0) = (cup x_0 (cup z_0 x_0)))), intros hyp.h_35,
apply (gapt.lk.CutRule ((cup z_0 x_0) = (cup x_0 z_0))), intros hyp.h_36,
exact sorry,
intros hyp.h_36,
apply (gapt.lk.EqualityRightRule2 (λ x : i, ((cup x_0 z_0) = (cup x_0 x))) (cup x_0 z_0) (cup z_0 x_0) hyp.h_36 hyp.h_35), intros hyp.h_37,
apply (gapt.lk.CutRule ((cup x_0 (cup x_0 z_0)) = (cup x_0 z_0))), intros hyp.h_38,
apply (gapt.lk.CutRule (x_0 = (cup x_0 x_0))), intros hyp.h_39,
apply (gapt.lk.CutRule ((cup x_0 x_0) = x_0)), intros hyp.h_40,
exact sorry,
intros hyp.h_40,
apply (gapt.lk.EqualityRightRule1 (λ x_2 : i, (x_2 = (cup x_0 x_0))) (cup x_0 x_0) x_0 hyp.h_40 hyp.h_39), intros hyp.h_41,
apply (gapt.lk.ReflexivityAxiom hyp.h_41), intros hyp.h_39,
apply (gapt.lk.EqualityRightRule2 (λ x : i, ((cup x_0 (cup x_0 z_0)) = (cup x z_0))) (cup x_0 x_0) x_0 hyp.h_39 hyp.h_38), intros hyp.h_40,
apply (gapt.lk.CutRule ((cup (cup x_0 x_0) z_0) = (cup x_0 (cup x_0 z_0)))), intros hyp.h_41,
exact sorry,
intros hyp.h_41,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, (x_1 = (cup (cup x_0 x_0) z_0))) (cup (cup x_0 x_0) z_0) (cup x_0 (cup x_0 z_0)) hyp.h_41 hyp.h_40), intros hyp.h_42,
apply (gapt.lk.ReflexivityAxiom hyp.h_42), intros hyp.h_38,
apply (gapt.lk.EqualityRightRule1 (λ x : i, (x = (cup x_0 (cup x_0 z_0)))) (cup x_0 (cup x_0 z_0)) (cup x_0 z_0) hyp.h_38 hyp.h_37), intros hyp.h_39,
apply (gapt.lk.ReflexivityAxiom hyp.h_39), intros hyp.h_35,
apply (gapt.lk.EqualityRightRule2 (λ x : i, ((cup z_0 (cup x_0 y_0)) = (cup z_0 x))) (cup x_0 (cup z_0 x_0)) (cup x_0 z_0) hyp.h_35 hyp.h_34), intros hyp.h_36,
apply (gapt.lk.CutRule ((cup z_0 (cup x_0 y_0)) = (cup (cup z_0 x_0) y_0))), intros hyp.h_37,
apply (gapt.lk.CutRule ((cup (cup z_0 x_0) y_0) = (cup z_0 (cup x_0 y_0)))), intros hyp.h_38,
exact sorry,
intros hyp.h_38,
apply (gapt.lk.EqualityRightRule1 (λ x_2 : i, (x_2 = (cup (cup z_0 x_0) y_0))) (cup (cup z_0 x_0) y_0) (cup z_0 (cup x_0 y_0)) hyp.h_38 hyp.h_37), intros hyp.h_39,
apply (gapt.lk.ReflexivityAxiom hyp.h_39), intros hyp.h_37,
apply (gapt.lk.EqualityRightRule2 (λ x : i, (x = (cup z_0 (cup x_0 (cup z_0 x_0))))) (cup (cup z_0 x_0) y_0) (cup z_0 (cup x_0 y_0)) hyp.h_37 hyp.h_36), intros hyp.h_38,
apply (gapt.lk.CutRule ((cup z_0 (cup x_0 (cup z_0 x_0))) = (cup (cup z_0 x_0) (cup z_0 x_0)))), intros hyp.h_39,
apply (gapt.lk.CutRule ((cup (cup z_0 x_0) (cup z_0 x_0)) = (cup z_0 (cup x_0 (cup z_0 x_0))))), intros hyp.h_40,
exact sorry,
intros hyp.h_40,
apply (gapt.lk.EqualityRightRule1 (λ x_2 : i, (x_2 = (cup (cup z_0 x_0) (cup z_0 x_0)))) (cup (cup z_0 x_0) (cup z_0 x_0)) (cup z_0 (cup x_0 (cup z_0 x_0))) hyp.h_40 hyp.h_39), intros hyp.h_41,
apply (gapt.lk.ReflexivityAxiom hyp.h_41), intros hyp.h_39,
apply (gapt.lk.EqualityRightRule2 (λ x : i, ((cup (cup z_0 x_0) y_0) = x)) (cup (cup z_0 x_0) (cup z_0 x_0)) (cup z_0 (cup x_0 (cup z_0 x_0))) hyp.h_39 hyp.h_38), intros hyp.h_40,
apply (gapt.lk.CutRule ((cup z_0 x_0) = (cup y_0 (cup z_0 x_0)))), intros hyp.h_41,
apply (gapt.lk.CutRule ((cup y_0 (cup z_0 x_0)) = (cup z_0 x_0))), intros hyp.h_42,
apply (gapt.lk.CutRule (z_0 = (cup y_0 z_0))), intros hyp.h_43,
apply (gapt.lk.EqualityRightRule1 (λ x : i, (x = (cup y_0 z_0))) (cup y_0 z_0) z_0 hyp.h_20 hyp.h_43), intros hyp.h_44,
apply (gapt.lk.ReflexivityAxiom hyp.h_44), intros hyp.h_43,
apply (gapt.lk.EqualityRightRule2 (λ x : i, ((cup y_0 (cup z_0 x_0)) = (cup x x_0))) (cup y_0 z_0) z_0 hyp.h_43 hyp.h_42), intros hyp.h_44,
apply (gapt.lk.CutRule ((cup (cup y_0 z_0) x_0) = (cup y_0 (cup z_0 x_0)))), intros hyp.h_45,
exact sorry,
intros hyp.h_45,
apply (gapt.lk.EqualityRightRule1 (λ x_2 : i, (x_2 = (cup (cup y_0 z_0) x_0))) (cup (cup y_0 z_0) x_0) (cup y_0 (cup z_0 x_0)) hyp.h_45 hyp.h_44), intros hyp.h_46,
apply (gapt.lk.ReflexivityAxiom hyp.h_46), intros hyp.h_42,
apply (gapt.lk.EqualityRightRule1 (λ x : i, (x = (cup y_0 (cup z_0 x_0)))) (cup y_0 (cup z_0 x_0)) (cup z_0 x_0) hyp.h_42 hyp.h_41), intros hyp.h_43,
apply (gapt.lk.ReflexivityAxiom hyp.h_43), intros hyp.h_41,
apply (gapt.lk.EqualityRightRule2 (λ x : i, ((cup (cup z_0 x_0) y_0) = (cup (cup z_0 x_0) x))) (cup y_0 (cup z_0 x_0)) (cup z_0 x_0) hyp.h_41 hyp.h_40), intros hyp.h_42,
apply (gapt.lk.CutRule ((cup y_0 (cup z_0 x_0)) = (cup (cup z_0 x_0) y_0))), intros hyp.h_43,
exact sorry,
intros hyp.h_43,
apply (gapt.lk.EqualityRightRule2 (λ x : i, ((cup (cup z_0 x_0) y_0) = (cup (cup z_0 x_0) x))) (cup (cup z_0 x_0) y_0) (cup y_0 (cup z_0 x_0)) hyp.h_43 hyp.h_42), intros hyp.h_44,
apply (gapt.lk.CutRule ((cup (cup z_0 x_0) (cup (cup z_0 x_0) y_0)) = (cup (cup z_0 x_0) y_0))), intros hyp.h_45,
apply (gapt.lk.CutRule ((cup z_0 x_0) = (cup (cup z_0 x_0) (cup z_0 x_0)))), intros hyp.h_46,
apply (gapt.lk.CutRule ((cup (cup z_0 x_0) (cup z_0 x_0)) = (cup z_0 x_0))), intros hyp.h_47,
exact sorry,
intros hyp.h_47,
apply (gapt.lk.EqualityRightRule1 (λ x_2 : i, (x_2 = (cup (cup z_0 x_0) (cup z_0 x_0)))) (cup (cup z_0 x_0) (cup z_0 x_0)) (cup z_0 x_0) hyp.h_47 hyp.h_46), intros hyp.h_48,
apply (gapt.lk.ReflexivityAxiom hyp.h_48), intros hyp.h_46,
apply (gapt.lk.EqualityRightRule2 (λ x : i, ((cup (cup z_0 x_0) (cup (cup z_0 x_0) y_0)) = (cup x y_0))) (cup (cup z_0 x_0) (cup z_0 x_0)) (cup z_0 x_0) hyp.h_46 hyp.h_45), intros hyp.h_47,
apply (gapt.lk.CutRule ((cup (cup (cup z_0 x_0) (cup z_0 x_0)) y_0) = (cup (cup z_0 x_0) (cup (cup z_0 x_0) y_0)))), intros hyp.h_48,
exact sorry,
intros hyp.h_48,
apply (gapt.lk.EqualityRightRule1 (λ x_1 : i, (x_1 = (cup (cup (cup z_0 x_0) (cup z_0 x_0)) y_0))) (cup (cup (cup z_0 x_0) (cup z_0 x_0)) y_0) (cup (cup z_0 x_0) (cup (cup z_0 x_0) y_0)) hyp.h_48 hyp.h_47), intros hyp.h_49,
apply (gapt.lk.ReflexivityAxiom hyp.h_49), intros hyp.h_45,
apply (gapt.lk.EqualityRightRule1 (λ x : i, (x = (cup (cup z_0 x_0) (cup (cup z_0 x_0) y_0)))) (cup (cup z_0 x_0) (cup (cup z_0 x_0) y_0)) (cup (cup z_0 x_0) y_0) hyp.h_45 hyp.h_44), intros hyp.h_46,
apply (gapt.lk.ReflexivityAxiom hyp.h_46), intros hyp.h_32,
apply (gapt.lk.EqualityRightRule1 (λ x : i, (x = (cup z_0 (cup x_0 y_0)))) (cup z_0 (cup x_0 y_0)) (cup z_0 x_0) hyp.h_32 hyp.h_31), intros hyp.h_33,
apply (gapt.lk.ReflexivityAxiom hyp.h_33), intros hyp.h_31,
apply (gapt.lk.EqualityLeftRule2 (λ x : i, (z_0 = x)) (cup z_0 (cup x_0 y_0)) (cup z_0 x_0) hyp.h_31 hyp.h_30), intros hyp.h_32,
apply (gapt.lk.CutRule ((cup (cup x_0 y_0) z_0) = (cup z_0 (cup x_0 y_0)))), intros hyp.h_33,
exact sorry,
intros hyp.h_33,
apply (gapt.lk.EqualityLeftRule1 (λ x : i, (z_0 = x)) (cup (cup x_0 y_0) z_0) (cup z_0 (cup x_0 y_0)) hyp.h_33 hyp.h_32), intros hyp.h_34,
apply (gapt.lk.EqualityRightRule1 (λ x : i, (x = z_0)) z_0 (cup (cup x_0 y_0) z_0) hyp.h_34 hyp.h_25), intros hyp.h_35,
apply (gapt.lk.ReflexivityAxiom hyp.h_35), intros hyp.h_25,
apply (gapt.lk.LogicalAxiom hyp.h_25 hyp.h_10), intros hyp.h_2,
apply (gapt.lk.AndLeftRule hyp.h_2), intros hyp.h_3 hyp.h_4,
apply (gapt.lk.AndLeftRule hyp.h_4), intros hyp.h_5 hyp.h_6,
apply (gapt.lk.AndLeftRule hyp.h_3), intros hyp.h_7 hyp.h_8,
apply (gapt.lk.AndLeftRule hyp.h_8), intros hyp.h_9 hyp.h_10,
apply (gapt.lk.AndRightRule hyp.h_1), intros hyp.h_10,
apply (gapt.lk.ForallRightRule hyp.h_10), intros x hyp.h_11,
apply (gapt.lk.ForallRightRule hyp.h_11), intros y hyp.h_12,
apply (gapt.lk.ForallLeftRule (cup (cap x y) x) hyp.h_9), intros hyp.h_13,
apply (gapt.lk.ForallLeftRule x hyp.h_13), intros hyp.h_14,
apply (gapt.lk.ImpLeftRule hyp.h_14), intros hyp.h_15,
apply (gapt.lk.ForallLeftRule (cap x y) hyp.h_6), intros hyp.h_16,
apply (gapt.lk.ForallLeftRule x hyp.h_16), intros hyp.h_17,
apply (gapt.lk.AndLeftRule hyp.h_17), intros hyp.h_18 hyp.h_19,
apply (gapt.lk.AndLeftRule hyp.h_18), intros hyp.h_20 hyp.h_21,
apply (gapt.lk.AndRightRule hyp.h_15), intros hyp.h_22,
apply (gapt.lk.ForallLeftRule x hyp.h_19), intros hyp.h_23,
apply (gapt.lk.ImpLeftRule hyp.h_23), intros hyp.h_24,
apply (gapt.lk.AndRightRule hyp.h_24), intros hyp.h_25,
apply (gapt.lk.ForallLeftRule x hyp.h_5), intros hyp.h_26,
apply (gapt.lk.ForallLeftRule y hyp.h_26), intros hyp.h_27,
apply (gapt.lk.AndLeftRule hyp.h_27), intros hyp.h_28 hyp.h_29,
apply (gapt.lk.AndLeftRule hyp.h_28), intros hyp.h_29 hyp.h_30,
apply (gapt.lk.LogicalAxiom hyp.h_29 hyp.h_25), intros hyp.h_25,
apply (gapt.lk.ForallLeftRule x hyp.h_7), intros hyp.h_26,
apply (gapt.lk.LogicalAxiom hyp.h_26 hyp.h_25), intros hyp.h_24,
apply (gapt.lk.LogicalAxiom hyp.h_24 hyp.h_22), intros hyp.h_22,
apply (gapt.lk.LogicalAxiom hyp.h_21 hyp.h_22), intros hyp.h_15,
apply (gapt.lk.LogicalAxiom hyp.h_15 hyp.h_12), intros hyp.h_10,
apply (gapt.lk.ForallRightRule hyp.h_10), intros x hyp.h_11,
apply (gapt.lk.ForallRightRule hyp.h_11), intros y hyp.h_12,
apply (gapt.lk.ForallLeftRule (cup x y) hyp.h_5), intros hyp.h_13,
apply (gapt.lk.ForallLeftRule x hyp.h_13), intros hyp.h_14,
apply (gapt.lk.AndLeftRule hyp.h_14), intros hyp.h_15 hyp.h_16,
apply (gapt.lk.AndLeftRule hyp.h_15), intros hyp.h_17 hyp.h_18,
apply (gapt.lk.ForallLeftRule (cap (cup x y) x) hyp.h_9), intros hyp.h_19,
apply (gapt.lk.ForallLeftRule x hyp.h_19), intros hyp.h_20,
apply (gapt.lk.ImpLeftRule hyp.h_20), intros hyp.h_21,
apply (gapt.lk.AndRightRule hyp.h_21), intros hyp.h_22,
apply (gapt.lk.LogicalAxiom hyp.h_18 hyp.h_22), intros hyp.h_22,
apply (gapt.lk.ForallLeftRule x hyp.h_16), intros hyp.h_23,
apply (gapt.lk.ImpLeftRule hyp.h_23), intros hyp.h_24,
apply (gapt.lk.AndRightRule hyp.h_24), intros hyp.h_25,
apply (gapt.lk.ForallLeftRule x hyp.h_6), intros hyp.h_26,
apply (gapt.lk.ForallLeftRule y hyp.h_26), intros hyp.h_27,
apply (gapt.lk.AndLeftRule hyp.h_27), intros hyp.h_28 hyp.h_29,
apply (gapt.lk.AndLeftRule hyp.h_28), intros hyp.h_29 hyp.h_30,
apply (gapt.lk.LogicalAxiom hyp.h_29 hyp.h_25), intros hyp.h_25,
apply (gapt.lk.ForallLeftRule x hyp.h_7), intros hyp.h_26,
apply (gapt.lk.LogicalAxiom hyp.h_26 hyp.h_25), intros hyp.h_24,
apply (gapt.lk.LogicalAxiom hyp.h_24 hyp.h_22), intros hyp.h_21,
apply (gapt.lk.LogicalAxiom hyp.h_21 hyp.h_12), end

end gapt_export