proposition: Lemma compMap_spec : forall (A B C D : Set)(eqdc : EqDec C)(eqdd : EqDec D)(P1 : A -> B -> Prop)(P2 : C -> D -> Prop)(lsa : list A)(lsb : list B)(c1 : A -> Comp C)(c2 : B -> Comp D), list_pred P1 lsa lsb -> (forall a b, In a lsa -> In b lsb -> P1 a b -> comp_spec P2 (c1 a) (c2 b)) -> comp_spec (list_pred P2) (compMap _ c1 lsa) (compMap _ c2 lsb).
proof: Proof. induction 1; intuition. unfold compMap. eapply comp_spec_ret. econstructor. simpl. eapply comp_spec_seq. apply nil. apply nil. eapply H1; simpl; intuition. intuition. eapply comp_spec_seq. eapply nil. eapply nil. eapply IHlist_pred. intuition. intuition. eapply comp_spec_ret. econstructor; eauto. Qed.
imports: FCF.FCF Permutation