proposition: Lemma fresh_distinct_vars_spec : forall n lv, let op := fresh_distinct_vars n lv in (no_repeats op) # (disjoint op lv) # length(op)=n.
proof: Proof. induction n as [ | n Hind]; introv. simpl; split; sp. allsimpl. pose proof (Hind ((fresh_var lv :: lv))) as Hind1; clear Hind. repnd. split; [| split]. - constructor; auto. apply disjoint_sym in Hind2. apply Hind2. left. auto. - apply disjoint_cons_l. split;[ | (apply fresh_var_not_in)]. apply disjoint_cons_r in Hind2. repnd; auto. - rewrite Hind1; reflexivity. Qed.
imports: list Omega