proposition: Theorem nat_double_ind (R : nat -> nat -> Type) (H1 : forall n, R 0 n) (H2 : forall n, R (S n) 0) (H3 : forall n m, R n m -> R (S n) (S m)) : forall n m:nat, R n m.
proof: Proof. simple_induction' n; auto. destruct m; auto. Defined.
imports: Basics Types Basics.Nat HoTT.DProp