proposition: Lemma par_construct_mergerest : forall Al bl P l, CPropToProp (par_construct Al bl) l /\ CPropToProp (par_mergerest Al bl P) l <-> CPropToProp (merge Al P) l.
proof: Proof. induction Al; intros bl P l; simpl; destruct bl; [easy.. |]. rewrite par_mergerest_decomp, merge_decomp. now case b; simpl; rewrite <-(IHAl bl). 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