whelp instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x:A. P x x.
whelp instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x,y:A. P x y \to P y x.
whelp instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x,y,z:A. P x y \to P y z \to P y z.
whelp instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x:A. P x x.
whelp instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x,y:A. P x y \to P y x.
whelp instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x,y,z:A. P x y \to P y z \to P y z.