proposition: Theorem typ_unique : forall e t T, typ e t T -> forall U : term, typ e t U -> conv T U.
proof: Proof. simple induction 1; intros. apply sym_conv. apply inv_typ_prop with e0; auto with coc core arith datatypes. apply sym_conv. apply inv_typ_set with e0; auto with coc core arith datatypes. apply inv_typ_ref with e0 U v; auto with coc core arith datatypes; intros. elim H1; intros. rewrite H5. elim fun_item with term U0 x e0 v; auto with coc core arith datatypes. apply inv_typ_abs with e0 T0 M U0; auto with coc core arith datatypes; intros. apply trans_conv_conv with (Prod T0 T1); auto with coc core arith datatypes. apply inv_typ_app with e0 u v U; auto with coc core arith datatypes; intros. apply trans_conv_conv with (subst v Ur0); auto with coc core arith datatypes. unfold subst in |- *; apply conv_conv_subst; auto with coc core arith datatypes. apply inv_conv_prod_r with V V0; auto with coc core arith datatypes. apply inv_typ_prod with e0 T0 U U0; auto with coc core arith datatypes; intros. apply trans_conv_conv with (Srt s3); auto with coc core arith datatypes. apply trans_conv_conv with U; auto with coc core arith datatypes. Qed.
imports: Termes Conv MyList