proposition: Lemma fv_ext : forall l : prt_names, name_unique l -> forall x : name, ~ In _ x l -> name_unique (x :: l).
proof: Proof. unfold name_unique in |- *; intros. generalize H2. inversion_clear H1; intros. inversion_clear H1; auto with coc core arith datatypes. elim H0. elim H3; auto with coc core arith datatypes. generalize H3. inversion_clear H1; intros. elim H0. elim H1; auto with coc core arith datatypes. elim H with n1 n0 x0; auto with coc core arith datatypes. Qed.
imports: Arith MyList MlTypes