proposition: Lemma leI_refl_morphism n: leI_of_leY (♢ n) = leI_refl _.
proof: Proof. induction n. now simpl. change (leI_refl n.+1) with (leI_raise_both (leI_refl n)). now rewrite <- IHn. Qed.
imports: Bonak(Notation) Bonak(LeInductive)