(fun x : Type => conj I ?Goal)