def f : Π (x : nat) (b : bool), bool = bool := λ bool, _

def g (heq : 1 == 1) := heq.symm
#print g