import logic

theorem tst (A B : Prop) : A ∧ B :=
and_intro sorry sorry