proposition: Lemma le_induction_base_computes {n P H_base H_step}: le_induction (♢ n) P H_base H_step = H_base.
proof: Proof. unfold le_induction, leYind_construct. rewrite leI_refl_morphism; simpl. now destruct leY_irrelevance. Qed.
imports: Bonak(Notation) Bonak(LeInductive)