proposition: Lemma le_induction_step_computes {n p P H_base H_step} {Hp: p.+1 <= n}: le_induction (↓ Hp) P H_base H_step = H_step p Hp (le_induction Hp P H_base H_step).
proof: Proof. invert_le Hp. unfold le_induction, leYind_construct. rewrite leI_down_morphism; simpl. now destruct leY_irrelevance. Qed.
imports: Bonak(Notation) Bonak(LeInductive)