Fix type validator for new let structure

coq/Infra/ExpressionAbbrevs.v

@@ -533,6 +533,60 @@ Proof.
   destruct (Q_orderedExps.exprCompare e3_1 e1) eqn:?; try congruence.
   destruct (Q_orderedExps.exprCompare e3_2 e2) eqn:?; try congruence.
 Qed.
+
+Lemma no_cycle_let_left e1:
+  forall e2 x m, Q_orderedExps.exprCompare e1 (Let m x e1 e2) <> Eq.
+Proof.
+  induction e1; intros *; cbn in *; try congruence.
+  destruct (mTypeEq m m0) eqn:?.
+  + destruct (n ?= x)%nat eqn:?; try congruence.
+    destruct (Q_orderedExps.exprCompare e1_1 (Let m n e1_1 e1_2)) eqn:?;
+             try congruence.
+  + destruct (n ?= x)%nat eqn:?; try congruence.
+    destruct (morePrecise m m0) eqn:?; unfold morePrecise in *;
+      destruct m; destruct m0; try congruence.
+    * rewrite Pos.leb_compare in *.
+      unfold mTypeEq in *.
+      rewrite POrderedType.Positive_as_OT.compare_antisym in Heqb0.
+      rewrite Pos.eqb_compare in *.
+      destruct (w ?= w0)%positive eqn:?; simpl; try congruence.
+      rewrite N.eqb_compare in *.
+      destruct (f ?= f0)%N eqn:?; simpl in *; congruence.
+    * rewrite Pos.leb_compare in *.
+      unfold mTypeEq in *.
+      rewrite POrderedType.Positive_as_OT.compare_antisym in Heqb0.
+      rewrite Pos.eqb_compare in *.
+      destruct (w ?= w0)%positive eqn:?; simpl; try congruence.
+      rewrite N.eqb_compare in *.
+      destruct (f ?= f0)%N eqn:?; simpl in *; congruence.
+Qed.
+
+Lemma no_cycle_let_right e2:
+  forall e1 x m, Q_orderedExps.exprCompare e2 (Let m x e1 e2) <> Eq.
+Proof.
+  induction e2; intros *; cbn in *; try congruence.
+  destruct (mTypeEq m m0) eqn:?.
+  + destruct (n ?= x)%nat eqn:?; try congruence.
+    destruct (Q_orderedExps.exprCompare e2_1 e1) eqn:?; try congruence.
+  + destruct (n ?= x)%nat eqn:?; try congruence.
+    destruct (morePrecise m m0) eqn:?; unfold morePrecise in *;
+      destruct m; destruct m0; try congruence.
+    * rewrite Pos.leb_compare in *.
+      unfold mTypeEq in *.
+      rewrite POrderedType.Positive_as_OT.compare_antisym in Heqb0.
+      rewrite Pos.eqb_compare in *.
+      destruct (w ?= w0)%positive eqn:?; simpl; try congruence.
+      rewrite N.eqb_compare in *.
+      destruct (f ?= f0)%N eqn:?; simpl in *; congruence.
+    * rewrite Pos.leb_compare in *.
+      unfold mTypeEq in *.
+      rewrite POrderedType.Positive_as_OT.compare_antisym in Heqb0.
+      rewrite Pos.eqb_compare in *.
+      destruct (w ?= w0)%positive eqn:?; simpl; try congruence.
+      rewrite N.eqb_compare in *.
+      destruct (f ?= f0)%N eqn:?; simpl in *; congruence.
+Qed.
+
 (*
 Lemma toRExpMap_toRTMap e Gamma m:
   toRExpMap Gamma (toRExp e) = Some m ->