proposition: Lemma Forall2_inv_length : forall A B (P:A->B->Prop) r s, Forall2 P r s -> length r = length s.
proof: Proof. Proof using. introv E. unfold length. lets*: Forall2_inv_length E. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)