proposition: Lemma inv_type_conv : forall (P : Prop) e t (U V : term), conv U V -> inv_type P e t U -> inv_type P e t V.
proof: Proof. do 6 intro. cut (forall x : term, conv V x -> conv U x). intro. case t; simpl in |- *; intros. generalize H1. elim s; auto with coc 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_conv_conv with V; auto with coc core arith datatypes. Qed.
imports: Termes Conv MyList