fact: Definition inv_Etype (P : Prop) (e : env) (t T : term) : Prop := match t with | Srt prop => Econv T (Srt kind) -> P | Srt set => Econv T (Srt kind) -> P | Srt kind => True | Ref n => forall x : term, item _ x e n -> Econv T (lift (S n) x) -> P | Abs A M => forall (s1 s2 : sort) (U : term), Etyp e A (Srt s1) -> Etyp (A :: e) M U -> Etyp (A :: e) U (Srt s2) -> Econv T (Prod A U) -> P | App u v => forall Ur V : term, Etyp e v V -> Etyp e u (Prod V Ur) -> Econv T (subst v Ur) -> P | Prod A B => forall s1 s2 : sort, Etyp e A (Srt s1) -> Etyp (A :: e) B (Srt s2) -> Econv T (Srt s2) -> P end.
imports: Termes Conv Ered MyList Types