Commit 4a21280d authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

WIP encore

parent 2d46a9a6
This diff is collapsed.
......@@ -66,7 +66,8 @@ Arguments Vars.union !_ !_.
Arguments Vars.inter !_ !_.
Arguments Vars.diff !_ !_.
Definition vars_of_list := fold_right Vars.add Vars.empty.
Definition vars_of_list : list variable -> Vars.t :=
fold_right Vars.add Vars.empty.
Fixpoint vars_unions (l: list Vars.t) :=
match l with
......@@ -106,13 +106,6 @@ Proof.
exists (S k). simpl in *. now rewrite Hk, Hk'.
Lemma subinvars_in sub v :
Vars.In v (Nam.subinvars sub) <-> In v (map fst sub).
induction sub as [|(x,t) sub IH]; simpl. varsdec.
VarsF.set_iff. intuition.
Lemma list_index_assoc vars v v' sub sub' n :
Inv vars sub sub' ->
list_index v (map fst sub) = Some n ->
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