proposition: Theorem fappendfDisjoint : forall (L1 L2 : list A) (HL1L2 : Disjoint L1 L2) (L3 : list A), Disjoint L1 L3 -> Disjoint L2 L3 -> Disjoint (fappendf L1 L2) L3.
proof: Proof. intros L1 L2 HL1L2 L3 H' H'0. apply appendDisjoint with (L1 := L1) (L2 := map f L2); auto. apply DisjointCom. apply Disjointf. apply DisjointCom; auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)