proposition: Lemma inv_Etyp_ref : forall (P : Prop) (e : env) (T : term) (n : nat), Etyp e (Ref n) T -> (forall U : term, item _ U e n -> Econv T (lift (S n) U) -> P) -> P.
proof: Proof. intros. apply Etyp_inversion with e (Ref n) T; simpl in |- *; intros; auto with coc ecoc core arith datatypes. apply H0 with x; auto with coc ecoc core arith datatypes. Qed.
imports: Termes Conv Ered MyList Types