Theorem T2 (a b : Bool) : a => b => a /\ b. done. done. apply imp_tactic. apply imp_tactic2. foo. apply imp_tactic. apply imp_tactic. apply conj_tactic. back. apply assumption_tactic. done.