(****************************************************************************) (* *) (* 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 sty0_defs. Inductive sty1 [g:G; c:C; t1:T]: T -> Prop := | sty1_sty0: (t2:?) (sty0 g c t1 t2) -> (sty1 g c t1 t2) | sty1_sing: (t:?) (sty1 g c t1 t) -> (t2:?) (sty0 g c t t2) -> (sty1 g c t1 t2). Hints Resolve sty1_sty0 : ld. Section sty1_props_base. (************************************************) Hints Resolve sty1_sing : ld. Theorem sty1_trans: (g:?; c:?; t1,t:?) (sty1 g c t1 t) -> (t2:?) (sty1 g c t t2) -> (sty1 g c t1 t2). Proof. Intros until 2; XElim H0; Clear t2; Intros; XDEAuto 2. Qed. Lemma sty1_bind: (g:?; b:?; c:?; v,t1,t2:?) (sty1 g (CHead c (Bind b) v) t1 t2) -> (sty1 g c (THead (Bind b) v t1) (THead (Bind b) v t2)). Proof. Intros until 1; XElim H; Clear t2; Intros; XDEAuto 3. Qed. Lemma sty1_appl: (g:?; c:?; v,t1,t2:?) (sty1 g c t1 t2) -> (sty1 g c (THead (Flat Appl) v t1) (THead (Flat Appl) v t2)). Proof. Intros until 1; XElim H; Clear t2; Intros; XDEAuto 3. Qed. End sty1_props_base. Hints Resolve sty1_bind sty1_appl : ld.