Draft of the rest of the compiling section.

ConcurrentLambda.v

@@ -2753,8 +2753,19 @@ Module InternalConcurrentLambda (Import E : Expression) (L : Locations) (LM : Lo
       auto with ConExpr.
   Qed.
 
+  Lemma LessNondetAntisym : forall E1 E2, LessNondet E1 E2 -> LessNondet E2 E1 -> E1 = E2.
+  Proof using.
+    intros E1 E2 lnd1; induction lnd1; intros lnd2; inversion lnd2; subst; 
+      repeat match goal with
+             | [IH : LessNondet ?E2 ?E1 -> ?E1 = ?E2,
+                     H : LessNondet ?E2 ?E1 |- _ ] =>
+               specialize (IH H); subst
+             end; auto.
+  Qed.
+
   Instance : Reflexive LessNondet := LessNondetRefl.
   Instance : Transitive LessNondet := LessNondetTrans.
+  Instance : Antisymmetric ConExpr (@eq ConExpr) LessNondet := LessNondetAntisym.
 
   Lemma MergeLessNondet : forall E1 E2 E,
       ConExprMerge E1 E2 = Some E ->
@@ -3325,25 +3336,13 @@ Module InternalConcurrentLambda (Import E : Expression) (L : Locations) (LM : Lo
     intros E1 E2 ξ lnd; revert ξ; induction lnd; intro ξ; cbn; eauto with ConExpr.
   Qed.
 
-  (* Lemma LessNondetSubst : forall E1 E2 σ1 σ2, *)
-  (*     LessNondet E1 E2 -> *)
-  (*     (forall n, LessNondet (σ1 n) (σ2 n)) -> *)
-  (*     LessNondet (E1 [ceg| σ1]) (E2 [ceg| σ2]). *)
-  (* Proof using. *)
-  (*   intros E1 E2 σ1 σ2 lnd; revert σ1 σ2; induction lnd; intros σ1 σ2 lnds; *)
-  (*     cbn; eauto with ConExpr. *)
-  (*   - apply LessNondetRecv. apply IHlnd. *)
-  (*     intro n; repeat rewrite ConExprLocalRenameSpec; apply LessNondetExprSubst; auto. *)
-  (*   - apply LessNondetLetRet. apply IHlnd1; auto. apply IHlnd2; auto. *)
-  (*     intro n; repeat rewrite ConExprLocalRenameSpec; apply LessNondetExprSubst; auto. *)
-  (*   - unfold GlobalUpSubst. apply LessNondetRecLocal. apply IHlnd. *)
-  (*     intro n; destruct n; auto with ConExpr. *)
-  (*     apply LessNondetRename. *)
-  (*     repeat rewrite ConExprLocalRenameSpec; apply LessNondetExprSubst; auto. *)
-  (*   - apply LessNondetRecGlobal. apply IHlnd. intro n. *)
-  (*     unfold GlobalUpSubst; do 2 (destruct n; auto with ConExpr). *)
-  (*     repeat apply LessNondetRename; auto. *)
-  (* Qed. *)
+  Lemma LessNondetSubst : forall E1 E2 σ,
+      LessNondet E1 E2 ->
+      LessNondet (E1 [ceg| σ]) (E2 [ceg| σ]).
+  Proof using.
+    intros E1 E2 σ lnd; revert σ; induction lnd; intros σ;
+      cbn; eauto with ConExpr.
+  Qed.
 
   Lemma LessNondetVals : forall V1 V2,
       LessNondet V1 V2 -> ConExprVal V1 \/ ConExprVal V2 -> V1 = V2.