proposition: Lemma compMap_eq : forall (A B : Set)(P : A -> B -> Prop)(C : Set)(eqd : EqDec C)(c1 : A -> Comp C)(c2 : B -> Comp C)(lsa : list A)(lsb : list B), list_pred P lsa lsb -> (forall a b, P a b -> forall x, evalDist (c1 a) x == evalDist (c2 b) x) -> forall x, evalDist (compMap _ c1 lsa) x == evalDist (compMap _ c2 lsb) x.
proof: Proof. induction 1; intuition. unfold compMap. intuition. unfold compMap. fold compMap. comp_skip. comp_skip. Qed.
imports: FCF.FCF