1 2 3 4 5 6 7 8 9 10
Axiom A : Type. Goal True. exact I. Check (fun P => P A). Abort. Goal True. Definition foo (A : Type) : Prop:= True. set (x:=foo). split. Qed.