proposition: Lemma X_le_change_right : forall x y y', X.eq y y' -> X_le_dec x y = X_le_dec x y'.
proof: Proof. intros. destruct (X_le_dec x y) eqn: eq. - rewrite X_le_sound in eq; inversion eq; clear eq. + symmetry. rewrite X_le_sound. left. eapply X.eq_trans; eauto. + symmetry. rewrite X_le_sound. right. eapply Raw.Proofs.MX.eq_lt; eauto; try reflexivity; rewrite <- H; auto. - symmetry. rewrite <- not_true_iff_false. intro. rewrite <- not_true_iff_false in eq. rewrite X_le_sound in eq, H0. inversion H0; clear H0. + symmetry in H. pose proof (X.eq_trans H1 H). tauto. + symmetry in H. pose proof (Raw.Proofs.MX.lt_eq H1 H). tauto. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.Arith.PeanoNat Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts