example : id (False → Nat) := by false_or_by_contra

example : id ((¬True → False) → True) := by false_or_by_contra