axiom.lean

def foo : x = y → Bool := Eq.rec true
theorem bar : False = PEmpty := propext ⟨False.elim, PEmpty.elim⟩
theorem baz : Quot.mk (fun _ _ => True) false = Quot.mk _ true := Quot.sound trivial
theorem qux : foo h = true := h.rec (motive := fun _ h => h.rec true = true) rfl

example : foo bar = true := rfl
example : foo baz = true := rfl
example : foo bar = true := qux
example : foo baz = true := qux