proposition: Theorem typ_inversion : forall (P : Prop) e t T, typ e t T -> inv_type P e t T -> P.
proof: Proof. simple induction 1; simpl in |- *; intros. auto with coc core arith datatypes. auto with coc core arith datatypes. elim H1; intros. apply H2 with x; auto with coc core arith datatypes. rewrite H3; auto with coc core arith datatypes. apply H6 with s1 s2 U; auto with coc core arith datatypes. apply H4 with Ur V; auto with coc core arith datatypes. apply H4 with s1 s2; auto with coc core arith datatypes. apply H1. apply inv_type_conv with V; auto with coc core arith datatypes. Qed.
imports: Termes Conv MyList