theorem self_implies_demo (P : Prop) : P → P := fun h => h