Check (forall x: nat, nat). Definition basic_truth : forall A : Prop, A -> A := fun (E : Prop)(x : E) => x. Check forall A : Prop, A. Check le. Check le 3 1. Check le_n. Check le_S. Check le_S 3. Check le_S 3 3 (le_n 3). Check le_S 3 4. Check le_S 3 4 (le_S 3 3 (le_n 3)). Fixpoint gen_rec (B : nat -> Type) (V : B 0) (F : forall p : nat, B p -> B (S p)) (n : nat) : B n := match n return B n with | O => V | S p => F p (gen_rec B V F p) end. Definition proof_0_le : forall x, 0 <= x := gen_rec (fun x => 0 <= x) (le_n 0) (le_S 0). Check proof_0_le 10. Compute proof_0_le 10. Inductive ge3 : nat -> Type := ge3n : ge3 3 | ge3S : forall m, ge3 m -> ge3 (S m). Check ge3S 3 ge3n. Check ge3S _ (ge3S _ (ge3S _ (ge3S _ (ge3S _ (ge3S _ (ge3S _ (ge3n))))))). Check (gen_rec (fun x=> ge3 (x + 3)) ge3n (fun m => ge3S (m + 3)) 7) : ge3 10. Fixpoint ge3_gen_rec (C : forall n : nat, ge3 n -> Type) (W : C 3 ge3n) (G : forall (n : nat) (t : ge3 n), C n t -> C (S n) (ge3S n t)) (m : nat) (g : ge3 m) := match g in ge3 k return C k g with | ge3n => W | ge3S p t => G p t (ge3_gen_rec C W G p t) end. Check ge3_gen_rec. Definition ge3_gen_ind : forall (P : nat -> Prop), P 3 -> (forall k, ge3 k -> P k -> P (S k)) -> forall (n : nat), ge3 n -> P n := fun P (V : P 3) (H : forall k, ge3 k -> P k -> P (S k)) => ge3_gen_rec (fun (x : nat) (t : ge3 x) => P x) V H. Inductive is3 : nat -> Prop := is3_refl : is3 3. Definition is3_gen (P : forall (x : nat), is3 x -> Type) (V : P 3 is3_refl) (y : nat) (t : is3 y) : P y t := match t in is3 k return P k t with | is3_refl => V end. Definition is3_gen_ind : forall P : nat -> Prop, P 3 -> forall x, is3 x -> P x := fun P V x t => match t in is3 x return P x with is3_refl => V end. Check is3_gen_ind. Definition is3_gen_ind : forall (P : nat -> Prop), P 3 -> forall y, is3 y -> P y := fun P (V : P 3) => is3_gen (fun x t => P x) V. Check is3_gen_ind. Inductive lt3 : nat -> Type := | lt3_0 : lt3 0 | lt3_1 : lt3 1 | lt3_2 : lt3 2. Definition lt3_gen (B : forall n : nat, lt3 n -> Type) (v0 : B 0 lt3_0) (v1 : B 1 lt3_1) (v2 : B 2 lt3_2) (x : nat) (t : lt3 x): B x t := match t in lt3 x return B x t with | lt3_0 => v0 | lt3_1 => v1 | lt3_2 => v2 end. Definition lt3_gen_ind (P : nat -> Prop) (V0 : P 0) (V1 : P 1) (V2 : P 2) (x : nat) : lt3 x -> P x := lt3_gen (fun (x : nat) (t : lt3 x) => P x) V0 V1 V2 x. Definition lt3_3_any : forall (x : nat) (P : Prop), lt3 (3 + x) -> P := fun (x : nat) (P : Prop) (t : lt3 (3 + x)) => lt3_gen_ind (fun x => match x with S (S (S k)) => P | _ => forall A : Prop, A -> A end) basic_truth basic_truth basic_truth (3 + x) t. Check lt3_3_any. Definition lt3pred x : lt3 x -> lt3 (pred x) := fun h : lt3 x => match h in lt3 x return lt3 (pred x) with | lt3_0 => lt3_0 | lt3_1 => lt3_0 | lt3_2 => lt3_1 end. Definition ge3Nlt3 (x : nat) : ge3 x -> lt3 x -> False := ge3_gen_ind (fun y => lt3 y -> False) (fun h : lt3 3 => (lt3_3_any 0 False h)) (fun (m : nat) (g3m : ge3 m) (ihm : lt3 m -> False) (fact : lt3 (S m)) => ihm (lt3pred (S m) fact)) x.