proposition: Lemma list_forall2_is_sound : forall (A B : Type) (f : A -> B -> bool) (l : list A) (l' : list B), list_forall2 f l l' = true <-> (length l = length l' /\ forall a b, In (a,b) (combine l l') -> f a b = true).
proof: Proof. intros A B f l; induction l as [ | a l]; destruct l' as [ | b l']. simpl; intuition. simpl; intuition; discriminate. simpl; intuition; discriminate. simpl; intuition. destruct (f a b); try discriminate; simpl in H; destruct (proj1 (IHl l') H) as [H' _]; rewrite H'; trivial. injection H1; intros; subst a0 b0; destruct (f a b); try discriminate; trivial. destruct (f a b); try discriminate; simpl in H; destruct (proj1 (IHl l') H) as [_ H']; apply H'; trivial. rewrite (H1 a b (or_introl _ (eq_refl _))); simpl. apply (proj2 (IHl l')); split. injection H0; trivial. intros; apply H1; right; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)