Inductive eq (A: Type) (a: A) : V (b: A). Type := | eqrefl: eq A a a. Implicite cons eq 1. Implicite eq 1. Inductive nat : Type := | O: nat | S: V (x: nat). nat. Inductive True : Type := | ITrue: True. Inductive False : Type :=. Definition Not (P: Type) := P -> False. Inductive And (A1: Type) (A2: Type) : Type := | conj: A1 -> A2 -> And A1 A2. Implicite cons And 2. Inductive Or (A1: Type) (A2: Type) : Type := | left: A1 -> Or A1 A2 | right: A2 -> Or A1 A2. Implicite cons Or 2. Inductive Exists (A: Type) (P: V (a: A). Type) : Type := | ex: V (a: A). V (H: P a). Exists A P. Implicite cons Exists 2. Inductive Decidable (P: Type) : Type := | IsTrue: P -> (Decidable P) | IsFalse: (Not P) -> (Decidable P). Implicite cons Decidable 1. Lemma nateqdec : V (x: nat). V (y: nat). Decidable (eq x y). intro. factorize x. apply natinduc; simpl; (repeat intro); destruct y. apply IsTrue. apply eqrefl. apply IsFalse; intro. destruct H. apply IsFalse; intro. destruct H. generalize Predindind10 x2 as H0; intro. destruct H0. destruct H2. apply IsTrue; apply @eqrefl. apply IsFalse; intro. apply H2. destruct H. apply eqrefl. Qed.