proposition: Theorem compose3 : forall hyps F (A B C D:Prop), (A -> B -> C -> D) -> (interp_ctx hyps F A) -> (interp_ctx hyps F B) -> (interp_ctx hyps F C) -> (interp_ctx hyps F D).
proof: Proof. induction F;intros A B C D H;simpl;auto. apply IHF;auto. Qed.
imports: List Bintree Bool BinPos