Commit 618f1d05 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

cleanup Alpha.v

parent 57b00fc1
This diff is collapsed.
......@@ -79,7 +79,7 @@ Definition vars_flatmap (f:string->Vars.t) (vs : Vars.t) :=
(** [fresh_var vars] : gives a new variable not in the set [vars]. *)
Fixpoint fresh_var_loop (vars:Vars.t) (id:string) n :=
Fixpoint fresh_var_loop (vars:Vars.t) (id:string) n : variable :=
match n with
| O => id
| S n => if negb (Vars.mem id vars) then id
......
......@@ -14,6 +14,11 @@ Hint Extern 10 => varsdec : set.
Arguments Vars.union !_ !_.
Lemma vars_mem_false x vs : ~Vars.In x vs -> Vars.mem x vs = false.
Proof.
rewrite <- Vars.mem_spec. now case Vars.mem.
Qed.
Lemma InA_In {A} x (l:list A) : InA eq x l <-> In x l.
Proof.
split.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment