(****************************************************************************) (* *) (* The formal system \lambda\delta *) (* *) (* Author: Ferruccio Guidi *) (* *) (* This file is distributed under the terms of the *) (* GNU General Public License Version 2 *) (* *) (****************************************************************************) Require Export pr0_defs. Inductive pr1 : T -> T -> Prop := | pr1_refl: (t:?) (pr1 t t) | pr1_sing: (t2,t1:?) (pr0 t1 t2) -> (t3:?) (pr1 t2 t3) -> (pr1 t1 t3). Hints Resolve pr1_refl : ld. Section pr1_props. (******************************************************) Hints Resolve pr1_sing : ld. Lemma pr1_pr0: (t1,t2:?) (pr0 t1 t2) -> (pr1 t1 t2). Proof. XDEAuto 2. Qed. Theorem pr1_t: (t2,t1:?) (pr1 t1 t2) -> (t3:?) (pr1 t2 t3) -> (pr1 t1 t3). Proof. Intros until 1; XElim H; XDEAuto 3. Qed. Lemma pr1_head_1: (u1,u2:?) (pr1 u1 u2) -> (t:?; k:?) (pr1 (THead k u1 t) (THead k u2 t)). Proof. Intros; XElim H; XDEAuto 3. Qed. Lemma pr1_head_2: (t1,t2:?) (pr1 t1 t2) -> (u:?; k:?) (pr1 (THead k u t1) (THead k u t2)). Proof. Intros; XElim H; XDEAuto 3. Qed. Hints Resolve pr1_head_1 pr1_head_2 : ld. Theorem pr1_comp: (v,w:?) (pr1 v w) -> (t,u:?) (pr1 t u) -> (k:?) (pr1 (THead k v t) (THead k w u)). Proof. Intros until 1; XElim H. (* case 1: pr1_refl *) XAuto. (* case 2: pr1_sing *) Intros; XElim H2; XDEAuto 3. Qed. End pr1_props. Hints Resolve pr1_pr0 pr1_head_1 pr1_head_2 pr1_comp : ld.