proposition: Lemma simplifyCProp_correct : forall p l, CPropToProp (simplifyCProp p) l <-> CPropToProp p l.
proof: Proof. split. - induction p; simpl; [easy.. |]. now destruct (simplifyCProp p1), (simplifyCProp p2); simpl; intros; (split; [apply IHp1 | apply IHp2]). - induction p; simpl; [easy.. |]. intros [H1 H2]. now destruct (simplifyCProp p1), (simplifyCProp p2); simpl in *; apply IHp1 in H1; apply IHp2 in H2; [easy | ..]; repeat split. Qed.
imports: Coq(Bool Floats Reals List Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations) Specific_bigint Specific_ops Interval_helper Float_full Prog Lang_expr