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