Nuprl - Pf lbl

1. x: Pattern
2. ground_ptn(x)
3. y: Pattern
4. ground_ptn(y)
5. x = y Label

x ~ y

By: Inst Thm* SQType(Pattern) [] THEN Unfold `sq_type` -1

Generated subgoal:

1 6. x,y:Pattern. x = y (x ~ y)
x ~ y

About: