proposition: Lemma merge_decomp : forall l1 p l, CPropToProp (merge l1 p) l <-> CPropToProp (merge l1 CTrue) l /\ CPropToProp p l.
proof: Proof. induction l1 as [| t l1]; [easy |]. simpl. intros p l. destruct_tuple_obj t. split; intros H. - apply IHl1 in H. destruct H as [H1 H]. simpl in H. destruct H as [h H]. split; apply IHl1. + now split; [| simpl]. + now apply IHl1. - destruct H as [H1 h]. apply IHl1 in H1. destruct H1 as [H1 H]. simpl in H. apply IHl1. now split; [| simpl]. 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