proposition: Theorem nat_double_ind : forall R:nat -> nat -> Prop, (forall n:nat, R 0 n) -> (forall n:nat, R (S n) 0) -> (forall n m:nat, R n m -> R (S n) (S m)) -> forall n m:nat, R n m.
proof: Proof. intros R ? ? ? n. induction n; auto. intro m; destruct m; auto. Qed.
imports: Notations Ltac Datatypes Logic