proposition: Lemma merge_Forall: forall (f:A->Prop) l1 l2, List.Forall f l1 -> List.Forall f l2 -> List.Forall f (merge (fun x y => bool_decide (x <= y)) l1 l2) .
proof: Proof. Proof with auto. intros f l1 l2. induction_merge l1 l2; intros ... - inversion_clear H1. constructor ... - inversion_clear H2. constructor ... Qed.
imports: Coq(List Wf_nat Recdef Compare_dec Arith Peano_dec Lia RelationClasses Sorting.Sorted Sorting.Permutation) hydras(DecPreOrder DecPreOrder_Instances Sort_spec)