(* Simple tests for multiple file handling *) Require a. Require b. Goal (A,B:Prop)(and A B) -> (and B A). Intros A B H. Induction H. Apply conj. Assumption. Assumption. Save and_comms_c.