proposition: Lemma nth_zip : forall (A B : Set)(lsa : list A)(lsb : list B) n a b defa defb, length lsa = length lsb -> nth n (zip lsa lsb) (defa, defb) = (a, b) -> nth n lsa defa = a /\ nth n lsb defb = b.
proof: Proof. induction lsa; destruct lsb; destruct n; intuition; simpl in *; try lia; try pairInv; intuition. inversion H; clear H; subst. eapply IHlsa. eauto. eauto. eapply IHlsa. eauto. eauto. Qed.
imports: FCF.FCF Permutation