proposition: Lemma inv_typ_ref : forall (P : Prop) e T n, typ e (Ref n) T -> (forall U : term, item _ U e n -> conv T (lift (S n) U) -> P) -> P.
proof: Proof. intros. apply typ_inversion with e (Ref n) T; simpl in |- *; intros; auto with coc core arith datatypes. apply H0 with x; auto with coc core arith datatypes. Qed.
imports: Termes Conv MyList