proposition: Lemma diagRecursion (f : nat -> nat -> Type) (init : ∏ n, f 0 n) (ind : ∏ m n, f m (S n) -> f (S m) n): ∏ m n, f m n.
proof: Proof. intros m. induction m as [|m H]. - exact init. - intros n. apply ind. apply H. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Univalence