PrintForm Definitions choice 1 Sections AutomataTheory Doc

At: comp choice 1 1 1 1
1. E: Prop
2. EquivRel x,y:. x E y
3. x,y:. Dec(x E y)
4. r:
5. x,y:. (x r y) (x E y)

(n,k:. (n E k) Min{ x | xrn } = Min{ x | xrk }) & (n:. n E Min{ x | xrn })
By: RWH (RevHypC 5) 0
Generated subgoal:

1 (n,k:. (n r k) Min{ x | xrn } = Min{ x | xrk }) & (n:. n r Min{ x | xrn })

About:
andallequalfunctionpropboolassert