proposition: Lemma inv_Etype_Econv : forall (P : Prop) (e : env) (t U V : term), Econv U V -> inv_Etype P e t U -> inv_Etype P e t V.
proof: Proof. do 6 intro. cut (forall x : term, Econv V x -> Econv U x). intro. case t; simpl in |- *; intros. generalize H1. elim s; auto with coc ecoc core arith datatypes; intros. apply H1 with x; auto with coc core arith datatypes. apply H1 with s1 s2 U0; auto with coc core arith datatypes. apply H1 with Ur V0; auto with coc core arith datatypes. apply H1 with s1 s2; auto with coc core arith datatypes. intros; apply trans_Econv_Econv with V; auto with coc core arith datatypes. Qed.
imports: Termes Conv Ered MyList Types