fact: Definition comp A B (merge : B -> B -> B) (l : B) (l' : @m A B) : @m A B := match l' with | left _ => right l | right l' => right (merge l l') end.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)