proposition: Lemma combine_eq : forall A B (L1:list A) (L2:list B), LibList.length L1 = LibList.length L2 -> combine L1 L2 = LibList.combine L1 L2.
proof: Proof. Proof using. introv E. gen L2. induction L1 as [|x1 L1']; intros; destruct L2 as [|x2 L2']; tryfalse. { auto. } { rew_list in E. rew_listx. simpl. fequals~. } Qed.
imports: TLC(LibTactics LibReflect)