proposition: Theorem plus_one_r' : forall n:nat, n + 1 = S n.
proof: Proof. Admitted. Inductive time : Type := | day | night. Check time_ind : forall P : time -> Prop, P day -> P night -> forall t : time, P t. Inductive rgb : Type := | red | green | blue. Check rgb_ind. Inductive natlist : Type := | nnil | ncons (n : nat) (l : natlist). Check natlist_ind : forall P : natlist -> Prop, P nnil -> (forall (n : nat) (l : natlist), P l -> P (ncons n l)) -> forall l : natlist, P l. Inductive natlist' : Type := | nnil' | nsnoc (l : natlist') (n : nat). Check natlist'_ind : forall P : natlist' -> Prop, P nnil' -> (forall l : natlist', P l -> forall n : nat, P (nsnoc l n)) -> forall n : natlist', P n. Inductive booltree : Type := | bt_empty | bt_leaf (b : bool) | bt_branch (b : bool) (t1 t2 : booltree). Definition booltree_property_type : Type := booltree -> Prop. Definition base_case (P : booltree_property_type) : Prop . Admitted. Definition leaf_case (P : booltree_property_type) : Prop . Admitted. Definition branch_case (P : booltree_property_type) : Prop . Admitted. Definition booltree_ind_type := forall (P : booltree_property_type), base_case P -> leaf_case P -> branch_case P -> forall (b : booltree), P b. Theorem booltree_ind_type_correct : booltree_ind_type. Proof. Admitted. Inductive Toy : Type := . Theorem Toy_correct : exists f g, forall P : Toy -> Prop, (forall b : bool, P (f b)) -> (forall (n : nat) (t : Toy), P t -> P (g n t)) -> forall t : Toy, P t. Proof. Admitted. Inductive tree (X:Type) : Type := | leaf (x : X) | node (t1 t2 : tree X). Check tree_ind. Inductive foo' (X:Type) : Type := | C1 (l : list X) (f : foo' X) | C2. Definition P_m0r (n:nat) : Prop := n * 0 = 0. Definition P_m0r' : nat -> Prop := fun n => n * 0 = 0. Theorem mul_0_r'' : forall n:nat, P_m0r n. Proof. apply nat_ind. - reflexivity. - intros n IHn. unfold P_m0r in IHn. unfold P_m0r. simpl. apply IHn. Qed.