proposition: Lemma lemma1 : El0 (induct (λ₁ u, I u)).
proof: Proof. unfold induct. refine (λ₀¹ x, λ₀ p, _). simplify. refine (λ₀ q,_). assert (El0 (I (λ₁ v, (sb v)·₁[U]·₁le'·₁x))) as h. { generalize (q·₀[λ₁ u, I u]·₀p). simplify. intros q'. exact q'. } refine (h·₀_). refine (λ₀¹ i,_). refine (λ₀ h', _). generalize (q·₀[λ₁ y, i ·₁ (λ₁ v, (sb v)·₁[U] ·₁ le' ·₁ y)]). simplify. intros q'. refine (q'·₀_). clear q'. unfold le at 1 in h'. simplify_in h'. unfold sb at 1 in h'. simplify_in h'. unfold le' at 1 in h'. simplify_in h'. exact h'. Qed.