proposition: Lemma leYind_construct {n p} Hp: leYind n p Hp.
proof: Proof. intros; induction (leI_of_leY Hp). - rewrite (leY_irrelevance Hp (♢ n)). exact (leYind_refl _). - rewrite (leY_irrelevance Hp (↓ (leY_of_leI l))). apply leYind_down, IHl. Defined.
imports: Bonak(Notation) Bonak(LeInductive)