Proof-term equivalence?

Stream: new members

[Chris M]

Lean has a propositional extensionality axiom. Does it also have "proof term equivalence":

axiom pte : forall P:Prop, forall x y : P,  x=y

[Anatole Dedecker]

This is called "proof-irrelevance" and it is built-in in the kernel. I'll let experts explain more

[Anatole Dedecker]

What I mean by "it is built in" is "Lean treats proofs of a same proposition as equal by definition". Look how the proof of docs#proof_irrel is just rfl, which means "true by definition"