diff --git a/.gitignore b/.gitignore
index 2b6f3f3..23c68e5 100644
--- a/.gitignore
+++ b/.gitignore
@@ -9,3 +9,7 @@
 *.blg
 *.ilg
 *.ind
+Makefile.coq
+*.glob
+*.v.d
+*.vo
diff --git a/BasicSyntax.v b/BasicSyntax.v
new file mode 100644
index 0000000..ed82e3f
--- /dev/null
+++ b/BasicSyntax.v
@@ -0,0 +1,250 @@
+(** Formal Reasoning About Programs <http://adam.chlipala.net/frap/>
+  * Chapter 2: Basic Program Syntax
+  * Author: Adam Chlipala
+  * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *)
+
+Require Import Frap.
+
+
+Module ArithWithConstants.
+
+  Inductive arith : Set :=
+  | Const (n : nat)
+  | Plus (e1 e2 : arith)
+  | Times (e1 e2 : arith).
+
+  Example ex1 := Const 42.
+  Example ex2 := Plus (Const 1) (Times (Const 2) (Const 3)).
+
+  Fixpoint size (e : arith) : nat :=
+    match e with
+    | Const _ => 1
+    | Plus e1 e2 => 1 + size e1 + size e2
+    | Times e1 e2 => 1 + size e1 + size e2
+    end.
+
+  Compute size ex1.
+  Compute size ex2.
+
+  Fixpoint depth (e : arith) : nat :=
+    match e with
+    | Const _ => 1
+    | Plus e1 e2 => 1 + max (depth e1) (depth e2)
+    | Times e1 e2 => 1 + max (depth e1) (depth e2)
+    end.
+
+  Compute depth ex1.
+  Compute size ex2.
+
+  Theorem depth_le_size : forall e, depth e <= size e.
+  Proof.
+    induct e.
+
+    simplify.
+    linear_arithmetic.
+
+    simplify.
+    linear_arithmetic.
+
+    simplify.
+    linear_arithmetic.
+  Qed.
+
+  Theorem depth_le_size_snazzy : forall e, depth e <= size e.
+  Proof.
+    induct e; simplify; linear_arithmetic.
+  Qed.
+
+  Fixpoint commuter (e : arith) : arith :=
+    match e with
+    | Const _ => e
+    | Plus e1 e2 => Plus (commuter e2) (commuter e1)
+    | Times e1 e2 => Times (commuter e2) (commuter e1)
+    end.
+
+  Compute commuter ex1.
+  Compute commuter ex2.
+
+  Theorem size_commuter : forall e, size (commuter e) = size e.
+  Proof.
+    induct e; simplify; linear_arithmetic.
+  Qed.
+
+  Theorem depth_commuter : forall e, depth (commuter e) = depth e.
+  Proof.
+    induct e; simplify; linear_arithmetic.
+  Qed.
+
+  Theorem commuter_inverse : forall e, commuter (commuter e) = e.
+  Proof.
+    induct e; simplify; equality.
+  Qed.
+
+End ArithWithConstants.
+
+Module ArithWithVariables.
+
+  Inductive arith : Set :=
+  | Const (n : nat)
+  | Var (x : var)
+  | Plus (e1 e2 : arith)
+  | Times (e1 e2 : arith).
+
+  Example ex1 := Const 42.
+  Example ex2 := Plus (Const 1) (Times (Var "x") (Const 3)).
+
+  Fixpoint size (e : arith) : nat :=
+    match e with
+    | Const _ => 1
+    | Var _ => 1
+    | Plus e1 e2 => 1 + size e1 + size e2
+    | Times e1 e2 => 1 + size e1 + size e2
+    end.
+
+  Compute size ex1.
+  Compute size ex2.
+
+  Fixpoint depth (e : arith) : nat :=
+    match e with
+    | Const _ => 1
+    | Var _ => 1
+    | Plus e1 e2 => 1 + max (depth e1) (depth e2)
+    | Times e1 e2 => 1 + max (depth e1) (depth e2)
+    end.
+
+  Compute depth ex1.
+  Compute size ex2.
+
+  Theorem depth_le_size : forall e, depth e <= size e.
+  Proof.
+    induct e; simplify; linear_arithmetic.
+  Qed.
+
+  Fixpoint commuter (e : arith) : arith :=
+    match e with
+    | Const _ => e
+    | Var _ => e
+    | Plus e1 e2 => Plus (commuter e2) (commuter e1)
+    | Times e1 e2 => Times (commuter e2) (commuter e1)
+    end.
+
+  Compute commuter ex1.
+  Compute commuter ex2.
+
+  Theorem size_commuter : forall e, size (commuter e) = size e.
+  Proof.
+    induct e; simplify; linear_arithmetic.
+  Qed.
+
+  Theorem depth_commuter : forall e, depth (commuter e) = depth e.
+  Proof.
+    induct e; simplify; linear_arithmetic.
+  Qed.
+
+  Theorem commuter_inverse : forall e, commuter (commuter e) = e.
+  Proof.
+    induct e; simplify; equality.
+  Qed.
+
+  Fixpoint substitute (inThis : arith) (replaceThis : var) (withThis : arith) : arith :=
+    match inThis with
+    | Const _ => inThis
+    | Var x => if x ==v replaceThis then withThis else inThis
+    | Plus e1 e2 => Plus (substitute e1 replaceThis withThis) (substitute e2 replaceThis withThis)
+    | Times e1 e2 => Times (substitute e1 replaceThis withThis) (substitute e2 replaceThis withThis)
+    end.
+
+  Theorem substitute_depth : forall replaceThis withThis inThis,
+    depth (substitute inThis replaceThis withThis) <= depth inThis + depth withThis.
+  Proof.
+    induct inThis.
+
+    simplify.
+    linear_arithmetic.
+
+    simplify.
+    cases (x ==v replaceThis).
+    linear_arithmetic.
+    simplify.
+    linear_arithmetic.
+
+    simplify.
+    linear_arithmetic.
+
+    simplify.
+    linear_arithmetic.
+  Qed.
+
+  Theorem substitute_depth_snazzy : forall replaceThis withThis inThis,
+    depth (substitute inThis replaceThis withThis) <= depth inThis + depth withThis.
+  Proof.
+    induct inThis; simplify;
+    try match goal with
+        | [ |- context[if ?a ==v ?b then _ else _] ] => cases (a ==v b); simplify
+        end; linear_arithmetic.
+  Qed.
+
+  Theorem substitute_self : forall replaceThis inThis,
+    substitute inThis replaceThis (Var replaceThis) = inThis.
+  Proof.
+    induct inThis; simplify;
+    try match goal with
+        | [ |- context[if ?a ==v ?b then _ else _] ] => cases (a ==v b); simplify
+        end; equality.
+  Qed.
+
+  Theorem substitute_commuter : forall replaceThis withThis inThis,
+    commuter (substitute inThis replaceThis withThis)
+    = substitute (commuter inThis) replaceThis (commuter withThis).
+  Proof.
+    induct inThis; simplify;
+    try match goal with
+        | [ |- context[if ?a ==v ?b then _ else _] ] => cases (a ==v b); simplify
+        end; equality.
+  Qed.
+
+  Fixpoint constantFold (e : arith) : arith :=
+    match e with
+    | Const _ => e
+    | Var _ => e
+    | Plus e1 e2 =>
+      let e1' := constantFold e1 in
+      let e2' := constantFold e2 in
+      match e1', e2' with
+      | Const n1, Const n2 => Const (n1 + n2)
+      | Const 0, _ => e2'
+      | _, Const 0 => e1'
+      | _, _ => Plus e1' e2'
+      end
+    | Times e1 e2 =>
+      let e1' := constantFold e1 in
+      let e2' := constantFold e2 in
+      match e1', e2' with
+      | Const n1, Const n2 => Const (n1 * n2)
+      | Const 1, _ => e2'
+      | _, Const 1 => e1'
+      | Const 0, _ => Const 0
+      | _, Const 0 => Const 0
+      | _, _ => Times e1' e2'
+      end
+    end.
+
+  Theorem size_constantFold : forall e, size (constantFold e) <= size e.
+  Proof.
+    induct e; simplify;
+    repeat match goal with
+           | [ |- context[match ?E with _ => _ end] ] => cases E; simplify
+           end; linear_arithmetic.
+  Qed.
+
+  Theorem commuter_constantFold : forall e, commuter (constantFold e) = constantFold (commuter e).
+  Proof.
+    induct e; simplify;
+    repeat match goal with
+           | [ |- context[match ?E with _ => _ end] ] => cases E; simplify
+           | [ H : ?f _ = ?f _ |- _ ] => invert H
+           | [ |- ?f _ = ?f _ ] => f_equal
+           end; equality || linear_arithmetic || ring.
+  Qed.
+
+End ArithWithVariables.
diff --git a/Frap.v b/Frap.v
new file mode 100644
index 0000000..c0a7a78
--- /dev/null
+++ b/Frap.v
@@ -0,0 +1,70 @@
+Require Import String Arith Omega Program Sets Relations Map Var Invariant.
+Export String Arith Sets Relations Map Var Invariant.
+Require Import List.
+Export ListNotations.
+Open Scope string_scope.
+
+Ltac inductN n :=
+  match goal with
+    | [ |- forall x : ?E, _ ] =>
+      match type of E with
+        | Prop =>
+          let H := fresh in intro H;
+            match n with
+              | 1 => dependent induction H
+              | S ?n' => inductN n'
+            end
+        | _ => intro; inductN n
+      end
+  end.
+
+Ltac induct e := inductN e || dependent induction e.
+
+Ltac invert' H := inversion H; clear H; subst.
+
+Ltac invertN n :=
+  match goal with
+    | [ |- forall x : ?E, _ ] =>
+      match type of E with
+        | Prop =>
+          let H := fresh in intro H;
+            match n with
+              | 1 => invert' H
+              | S ?n' => invertN n'
+            end
+        | _ => intro; invertN n
+      end
+  end.
+
+Ltac invert e := invertN e || invert' e.
+
+Ltac invert0 e := invert e; fail.
+Ltac invert1 e := invert0 e || (invert e; []).
+Ltac invert2 e := invert1 e || (invert e; [|]).
+
+Ltac simplify := simpl in *.
+
+Ltac linear_arithmetic :=
+    repeat match goal with
+           | [ |- context[max ?a ?b] ] =>
+             let Heq := fresh "Heq" in destruct (Max.max_spec a b) as [[? Heq] | [? Heq]];
+               rewrite Heq in *; clear Heq
+           | [ _ : context[max ?a ?b] |- _ ] =>
+             let Heq := fresh "Heq" in destruct (Max.max_spec a b) as [[? Heq] | [? Heq]];
+               rewrite Heq in *; clear Heq
+           | [ |- context[min ?a ?b] ] =>
+             let Heq := fresh "Heq" in destruct (Min.min_spec a b) as [[? Heq] | [? Heq]];
+               rewrite Heq in *; clear Heq
+           | [ _ : context[min ?a ?b] |- _ ] =>
+             let Heq := fresh "Heq" in destruct (Min.min_spec a b) as [[? Heq] | [? Heq]];
+               rewrite Heq in *; clear Heq
+           end; omega.
+
+Ltac equality := congruence.
+
+Ltac cases E :=
+  (is_var E; destruct E)
+  || match type of E with
+     | {_} + {_} => destruct E
+     | _ => let Heq := fresh "Heq" in destruct E eqn:Heq
+     end.
diff --git a/Invariant.v b/Invariant.v
new file mode 100644
index 0000000..0ff66bb
--- /dev/null
+++ b/Invariant.v
@@ -0,0 +1,30 @@
+Require Import Relations.
+
+Set Implicit Arguments.
+
+
+Section Invariant.
+  Variable state : Type.
+  Variable step : state -> state -> Prop.
+  Variable invariant : state -> Prop.
+
+  Hint Constructors trc.
+
+  Definition safe (s : state) :=
+    forall s', step^* s s' -> invariant s'.
+
+  Variable s0 : state.
+
+  Hypothesis Hinitial : invariant s0.
+
+  Hypothesis Hstep : forall s s', invariant s -> step s s' -> invariant s'.
+
+  Lemma safety : safe s0.
+  Proof.
+    generalize dependent s0.
+    unfold safe.
+    induction 2; eauto.
+  Qed.
+End Invariant.
+
+Hint Resolve safety.
diff --git a/Makefile b/Makefile
index f96a0a0..79ef23d 100644
--- a/Makefile
+++ b/Makefile
@@ -1,6 +1,20 @@
+.PHONY: all coq
+
+all: frap.pdf coq
+
 frap.pdf: frap.tex Makefile
 	pdflatex frap
 	pdflatex frap
 	makeindex frap
 	pdflatex frap
 	pdflatex frap
+
+coq: Makefile.coq
+	$(MAKE) -f Makefile.coq
+
+Makefile.coq: Makefile _CoqProject *.v
+	coq_makefile -f _CoqProject -o Makefile.coq
+
+clean:: Makefile.coq
+	$(MAKE) -f Makefile.coq clean
+	rm -f Makefile.coq
diff --git a/Map.v b/Map.v
new file mode 100644
index 0000000..77f1aea
--- /dev/null
+++ b/Map.v
@@ -0,0 +1,216 @@
+Require Import Classical Sets ClassicalEpsilon FunctionalExtensionality.
+
+Set Implicit Arguments.
+
+Module Type S.
+  Parameter map : Type -> Type -> Type.
+
+  Parameter empty : forall A B, map A B.
+  Parameter add : forall A B, map A B -> A -> B -> map A B.
+  Parameter join : forall A B, map A B -> map A B -> map A B.
+  Parameter lookup : forall A B, map A B -> A -> option B.
+  Parameter includes : forall A B, map A B -> map A B -> Prop.
+
+  Notation "$0" := (empty _ _).
+  Notation "m $+ ( k , v )" := (add m k v) (at level 50, left associativity).
+  Infix "$++" := join (at level 50, left associativity).
+  Infix "$?" := lookup (at level 50, no associativity).
+  Infix "$<=" := includes (at level 90).
+
+  Parameter dom : forall A B, map A B -> set A.
+
+  Axiom map_ext : forall A B (m1 m2 : map A B),
+    (forall k, m1 $? k = m2 $? k)
+    -> m1 = m2.
+
+  Axiom lookup_empty : forall A B k, empty A B $? k = None.
+
+  Axiom includes_lookup : forall A B (m m' : map A B) k v,
+    m $? k = Some v
+    -> m $<= m'
+    -> lookup m' k = Some v.
+
+  Axiom includes_add : forall A B (m m' : map A B) k v,
+    m $<= m'
+    -> add m k v $<= add m' k v.
+
+  Axiom lookup_add_eq : forall A B (m : map A B) k v,
+    add m k v $? k = Some v.
+
+  Axiom lookup_add_ne : forall A B (m : map A B) k k' v,
+    k' <> k
+    ->  add m k v $? k' = m $? k'.
+
+  Axiom lookup_join1 : forall A B (m1 m2 : map A B) k,
+    k \in dom m1
+    -> (m1 $++ m2) $? k = m1 $? k.
+
+  Axiom lookup_join2 : forall A B (m1 m2 : map A B) k,
+    ~k \in dom m1
+    -> (m1 $++ m2) $? k = m2 $? k.
+
+  Axiom join_comm : forall A B (m1 m2 : map A B),
+    dom m1 \cap dom m2 = {}
+    -> m1 $++ m2 = m2 $++ m1.
+
+  Axiom join_assoc : forall A B (m1 m2 m3 : map A B),
+    (m1 $++ m2) $++ m3 = m1 $++ (m2 $++ m3).
+
+  Axiom empty_includes : forall A B (m : map A B), empty A B $<= m.
+
+  Axiom dom_empty : forall A B, dom (empty A B) = {}.
+
+  Axiom dom_add : forall A B (m : map A B) (k : A) (v : B),
+    dom (add m k v) = {k} \cup dom m.
+
+  Hint Extern 1 => match goal with
+                     | [ H : lookup (empty _ _) _ = Some _ |- _ ] =>
+                       rewrite lookup_empty in H; discriminate
+                   end.
+
+  Hint Resolve includes_lookup includes_add empty_includes.
+
+  Hint Rewrite lookup_add_eq lookup_add_ne using congruence.
+
+  Ltac maps_equal :=
+    apply map_ext; intros;
+      repeat (subst; autorewrite with core; try reflexivity;
+        match goal with
+          | [ |- context[lookup (add _ ?k _) ?k' ] ] => destruct (classic (k = k')); subst
+        end).
+
+  Hint Extern 3 (_ = _) => maps_equal.
+End S.
+
+Module M : S.
+  Definition map (A B : Type) := A -> option B.
+
+  Definition empty A B : map A B := fun _ => None.
+
+  Section decide.
+    Variable P : Prop.
+
+    Lemma decided : inhabited (sum P (~P)).
+    Proof.
+      destruct (classic P).
+      constructor; exact (inl _ H).
+      constructor; exact (inr _ H).
+    Qed.
+
+    Definition decide : sum P (~P) :=
+      epsilon decided (fun _ => True).
+  End decide.
+
+  Definition add A B (m : map A B) (k : A) (v : B) : map A B :=
+    fun k' => if decide (k' = k) then Some v else m k'.
+  Definition join A B (m1 m2 : map A B) : map A B :=
+    fun k => match m1 k with
+               | None => m2 k
+               | x => x
+             end.
+  Definition lookup A B (m : map A B) (k : A) := m k.
+  Definition includes A B (m1 m2 : map A B) :=
+    forall k v, m1 k = Some v -> m2 k = Some v.
+
+  Definition dom A B (m : map A B) : set A := fun x => m x <> None.
+
+  Theorem map_ext : forall A B (m1 m2 : map A B),
+    (forall k, lookup m1 k = lookup m2 k)
+    -> m1 = m2.
+  Proof.
+    intros; extensionality k; auto.
+  Qed.
+
+  Theorem lookup_empty : forall A B (k : A), lookup (empty B) k = None.
+  Proof.
+    auto.
+  Qed.
+
+  Theorem includes_lookup : forall A B (m m' : map A B) k v,
+    lookup m k = Some v
+    -> includes m m'
+    -> lookup m' k = Some v.
+  Proof.
+    auto.
+  Qed.
+
+  Theorem includes_add : forall A B (m m' : map A B) k v,
+    includes m m'
+    -> includes (add m k v) (add m' k v).
+  Proof.
+    unfold includes, add; intuition.
+    destruct (decide (k0 = k)); auto.
+  Qed.
+
+  Theorem lookup_add_eq : forall A B (m : map A B) k v,
+    lookup (add m k v) k = Some v.
+  Proof.
+    unfold lookup, add; intuition.
+    destruct (decide (k = k)); tauto.
+  Qed.
+
+  Theorem lookup_add_ne : forall A B (m : map A B) k k' v,
+    k' <> k
+    -> lookup (add m k v) k' = lookup m k'.
+  Proof.
+    unfold lookup, add; intuition.
+    destruct (decide (k' = k)); intuition.
+  Qed.
+
+  Theorem lookup_join1 : forall A B (m1 m2 : map A B) k,
+    k \in dom m1
+    -> lookup (join m1 m2) k = lookup m1 k.
+  Proof.
+    unfold lookup, join, dom, In; intros.
+    destruct (m1 k); congruence.
+  Qed.
+
+  Theorem lookup_join2 : forall A B (m1 m2 : map A B) k,
+    ~k \in dom m1
+    -> lookup (join m1 m2) k = lookup m2 k.
+  Proof.
+    unfold lookup, join, dom, In; intros.
+    destruct (m1 k); try congruence.
+    exfalso; apply H; congruence.
+  Qed.
+
+  Theorem join_comm : forall A B (m1 m2 : map A B),
+    dom m1 \cap dom m2 = {}
+    -> join m1 m2 = join m2 m1.
+  Proof.
+    intros; apply map_ext; unfold join, lookup; intros.
+    apply (f_equal (fun f => f k)) in H.
+    unfold dom, intersection, constant in H; simpl in H.
+    destruct (m1 k), (m2 k); auto.
+    exfalso; rewrite <- H.
+    intuition congruence.
+  Qed.
+
+  Theorem join_assoc : forall A B (m1 m2 m3 : map A B),
+    join (join m1 m2) m3 = join m1 (join m2 m3).
+  Proof.
+    intros; apply map_ext; unfold join, lookup; intros.
+    destruct (m1 k); auto.
+  Qed.
+
+  Theorem empty_includes : forall A B (m : map A B), includes (empty (A := A) B) m.
+  Proof.
+    unfold includes, empty; intuition congruence.
+  Qed.
+
+  Theorem dom_empty : forall A B, dom (empty (A := A) B) = {}.
+  Proof.
+    unfold dom, empty; intros; sets idtac.
+  Qed.
+
+  Theorem dom_add : forall A B (m : map A B) (k : A) (v : B),
+    dom (add m k v) = {k} \cup dom m.
+  Proof.
+    unfold dom, add; simpl; intros.
+    sets ltac:(simpl in *; try match goal with
+                                 | [ _ : context[if ?E then _ else _] |- _ ] => destruct E
+                               end; intuition congruence).
+  Qed.
+End M.
+
+Export M.
diff --git a/Relations.v b/Relations.v
new file mode 100644
index 0000000..9454813
--- /dev/null
+++ b/Relations.v
@@ -0,0 +1,122 @@
+Set Implicit Arguments.
+
+
+Section trc.
+  Variable A : Type.
+  Variable R : A -> A -> Prop.
+
+  Inductive trc : A -> A -> Prop :=
+  | TrcRefl : forall x, trc x x
+  | TrcFront : forall x y z,
+    R x y
+    -> trc y z
+    -> trc x z.
+
+  Hint Constructors trc.
+
+  Theorem trc_trans : forall x y, trc x y
+    -> forall z, trc y z
+      -> trc x z.
+  Proof.
+    induction 1; eauto.
+  Qed.
+
+  Hint Resolve trc_trans.
+
+  Inductive trcEnd : A -> A -> Prop :=
+  | TrcEndRefl : forall x, trcEnd x x
+  | TrcBack : forall x y z,
+    trcEnd x y
+    -> R y z
+    -> trcEnd x z.
+
+  Hint Constructors trcEnd.
+
+  Lemma TrcFront' : forall x y z,
+    R x y
+    -> trcEnd y z
+    -> trcEnd x z.
+  Proof.
+    induction 2; eauto.
+  Qed.
+
+  Hint Resolve TrcFront'.
+
+  Theorem trc_trcEnd : forall x y, trc x y
+    -> trcEnd x y.
+  Proof.
+    induction 1; eauto.
+  Qed.
+
+  Hint Resolve trc_trcEnd.
+
+  Lemma TrcBack' : forall x y z,
+    trc x y
+    -> R y z
+    -> trc x z.
+  Proof.
+    induction 1; eauto.
+  Qed.
+
+  Hint Resolve TrcBack'.
+
+  Theorem trcEnd_trans : forall x y, trcEnd x y
+    -> forall z, trcEnd y z
+      -> trcEnd x z.
+  Proof.
+    induction 1; eauto.
+  Qed.
+
+  Hint Resolve trcEnd_trans.
+  
+  Theorem trcEnd_trc : forall x y, trcEnd x y
+    -> trc x y.
+  Proof.
+    induction 1; eauto.
+  Qed.
+
+  Hint Resolve trcEnd_trc.
+
+  Inductive trcLiteral : A -> A -> Prop :=
+  | TrcLiteralRefl : forall x, trcLiteral x x
+  | TrcTrans : forall x y z, trcLiteral x y
+    -> trcLiteral y z
+    -> trcLiteral x z
+  | TrcInclude : forall x y, R x y
+    -> trcLiteral x y.
+
+  Hint Constructors trcLiteral.
+
+  Theorem trc_trcLiteral : forall x y, trc x y
+    -> trcLiteral x y.
+  Proof.
+    induction 1; eauto.
+  Qed.
+
+  Theorem trcLiteral_trc : forall x y, trcLiteral x y
+    -> trc x y.
+  Proof.
+    induction 1; eauto.
+  Qed.
+
+  Hint Resolve trc_trcLiteral trcLiteral_trc.
+
+  Theorem trcEnd_trcLiteral : forall x y, trcEnd x y
+    -> trcLiteral x y.
+  Proof.
+    induction 1; eauto.
+  Qed.
+
+  Theorem trcLiteral_trcEnd : forall x y, trcLiteral x y
+    -> trcEnd x y.
+  Proof.
+    induction 1; eauto.
+  Qed.
+
+  Hint Resolve trcEnd_trcLiteral trcLiteral_trcEnd.
+End trc.
+
+Notation "R ^*" := (trc R) (at level 0).
+Notation "*^ R" := (trcEnd R) (at level 0).
+
+Hint Constructors trc.
diff --git a/Sets.v b/Sets.v
new file mode 100644
index 0000000..7df06d3
--- /dev/null
+++ b/Sets.v
@@ -0,0 +1,117 @@
+Require Import Classical FunctionalExtensionality List.
+
+Set Implicit Arguments.
+
+
+Axiom prop_ext : forall P Q : Prop,
+  (P <-> Q) -> P = Q.
+
+Section set.
+  Variable A : Type.
+
+  Definition set := A -> Prop.
+  Definition In (x : A) (s : set) := s x.
+
+  Definition constant (ls : list A) : set := fun x => List.In x ls.
+  Definition universe : set := fun _ => True.
+  Definition check (P : Prop) : set := fun _ => P.
+
+  Definition union (s1 s2 : set) : set := fun x => s1 x \/ s2 x.
+  Definition intersection (s1 s2 : set) : set := fun x => s1 x /\ s2 x.
+  Definition complement (s : set) : set := fun x => ~s x.
+
+  Definition subseteq (s1 s2 : set) := forall x, s1 x -> s2 x.
+  Definition subset (s1 s2 : set) := subseteq s1 s2 /\ ~subseteq s2 s1.
+
+  Definition scomp (P : A -> Prop) : set := P.
+
+  Theorem sets_equal : forall s1 s2 : set, (forall x, s1 x <-> s2 x) -> s1 = s2.
+  Proof.
+    intros.
+    apply functional_extensionality; intros.
+    apply prop_ext; auto.
+  Qed.
+End set.
+
+Infix "\in" := In (at level 70).
+Notation "{ }" := (constant nil).
+Notation "{ x1 , .. , xN }" := (constant (cons x1 (.. (cons xN nil) ..))).
+Notation "[ P ]" := (check P).
+Infix "\cup" := union (at level 40).
+Infix "\cap" := intersection (at level 40).
+Infix "\subseteq" := subseteq (at level 70).
+Infix "\subset" := subset (at level 70).
+Notation "[ x | P ]" := (scomp (fun x => P)).
+
+Ltac sets' tac :=
+  unfold In, constant, universe, check, union, intersection, complement, subseteq, subset, scomp in *;
+    tauto || intuition tac.
+
+Ltac sets tac :=
+  try match goal with
+        | [ |- @eq (set _) _ _ ] => apply sets_equal; intro; split
+      end; sets' tac.
+
+
+(** * Some of the usual properties of set operations *)
+
+Section properties.
+  Variable A : Type.
+  Variable x : A.
+  Variables s1 s2 s3 : set A.
+
+  Theorem union_comm : s1 \cup s2 = s2 \cup s1.
+  Proof.
+    sets idtac.
+  Qed.
+
+  Theorem union_assoc : (s1 \cup s2) \cup s3 = s1 \cup (s2 \cup s3).
+  Proof.
+    sets idtac.
+  Qed.
+
+  Theorem intersection_comm : s1 \cap s2 = s2 \cap s1.
+  Proof.
+    sets idtac.
+  Qed.
+
+  Theorem intersection_assoc : (s1 \cap s2) \cap s3 = s1 \cap (s2 \cap s3).
+  Proof.
+    sets idtac.
+  Qed.
+
+  Theorem not_union : complement (s1 \cup s2) = complement s1 \cap complement s2.
+  Proof.
+    sets idtac.
+  Qed.
+
+  Theorem not_intersection : complement (s1 \cap s2) = complement s1 \cup complement s2.
+  Proof.
+    sets idtac.
+  Qed.
+
+  Theorem subseteq_refl : s1 \subseteq s1.
+  Proof.
+    unfold subseteq; eauto.
+  Qed.
+
+  Theorem subseteq_In : s1 \subseteq s2 -> x \in s1 -> x \in s2.
+  Proof.
+    unfold subseteq, In; eauto.
+  Qed.
+
+  Theorem cap_split : forall (P1 P2 : A -> Prop),
+    (forall s, P1 s \/ P2 s)
+    -> s1 \cap [s | P1 s] \subseteq s2
+    -> s1 \cap [s | P2 s] \subseteq s3
+    -> s1 \subseteq (s2 \cap [s | P1 s]) \cup (s3 \cap [s | P2 s]).
+  Proof.
+    intros; sets eauto.
+    specialize (H x0).
+    specialize (H0 x0).
+    specialize (H1 x0).
+    tauto.
+  Qed.
+End properties.
+
+Hint Resolve subseteq_refl subseteq_In.
diff --git a/Var.v b/Var.v
new file mode 100644
index 0000000..b042217
--- /dev/null
+++ b/Var.v
@@ -0,0 +1,7 @@
+Require Import String.
+
+
+Definition var := string.
+Definition var_eq : forall x y : var, {x = y} + {x <> y} := string_dec.
+
+Infix "==v" := var_eq (no associativity, at level 50).
diff --git a/_CoqProject b/_CoqProject
new file mode 100644
index 0000000..9604142
--- /dev/null
+++ b/_CoqProject
@@ -0,0 +1,7 @@
+-R . Frap
+Map.v
+Var.v
+Sets.v
+Relations.v
+Frap.v
+BasicSyntax.v