だんだん込み入ってきた。
Include "../usr/guru-lang/lib/nat.g".
Include "../usr/guru-lang/lib/plus.g".
Define plusZ' :=
foralli(x:nat)(u : {x = Z}).
trans cong (plus * *) u % (plus x x) = (plus Z Z)
join (plus Z Z) Z. % (plus Z Z) = Z
Define ltcomm : Forall(x:nat).Exists(y:nat). { (le x y) = (le y x) } :=
foralli(x:nat).
existsi x { (le x *) = (le * x) } refl (le x x).
Define existsle : Forall(x:nat).Exists(y:nat). { (le x y) = tt } :=
foralli(x:nat).
existsi x { (le x *) = tt } [x_le_x x]. % [x_le_x x] -> {(le x x) = tt}
Define existslt : Forall(x:nat). Exists(z:nat). {(lt x z) = tt } :=
foralli(x:nat). % 1.Introduce our arbitrary x of type nat.
existse
[existsle x] % Exists(y : nat) . { (le x y) = tt }
foralli(y:nat)(u:{(le x y) = tt}). % Forall(x:T)(u:F).
existsi (S y) { (lt x *) = tt } % F'
[lelt_trans x y (S y) u [lt_S y]]. % {(lt x (S y)) = tt }
Classify foralli(x:nat).[existsle x].
