proposition: Lemma merge_equation: forall l1 l2, merge (fun x y => bool_decide (x <= y)) l1 l2 = match l1,l2 with | nil,_ => l2 | _,nil => l1 | a1::l1',a2::l2' => if decide (a1 <= a2) then a1 :: merge (fun x y => bool_decide (x <= y)) l1' l2 else a2 :: merge (fun x y => bool_decide (x <= y)) l1 l2' end.
proof: Proof. intros l1 l2. induction_merge l1 l2; trivial. - now intros l; destruct l. - intros a1 l1' a2 l2' Comp Eq. destruct (decide (a1 <= a2)); [reflexivity|contradiction]. - intros a1 l1' a2 l2' Comp Eq. destruct (decide (a1 <= a2)); [contradiction|reflexivity]. Qed.
imports: Coq(List Wf_nat Recdef Compare_dec Arith Peano_dec Lia RelationClasses Sorting.Sorted Sorting.Permutation) hydras(DecPreOrder DecPreOrder_Instances Sort_spec)