Nuprl - Pf list_quo

PrintForm Definitions automata 5 Sections AutomataTheory Doc

q:, E:(q*q*Prop). (EquivRel x,y:q*. x E y) & (x,y:q*. Dec(x E y)) (h:(q*q*). (x,y:q*. (x E y) h(x) = h(y)) & (x:q*. x E (h(x))))

By: Analyze 0 THEN Decide (0 < q)

Generated subgoals:

1 1. q:
2. 0 < q
E:(q*q*Prop). (EquivRel x,y:q*. x E y) & (x,y:q*. Dec(x E y)) (h:(q*q*). (x,y:q*. (x E y) h(x) = h(y)) & (x:q*. x E (h(x))))

2 1. q:
2. 0 < q
E:(q*q*Prop). (EquivRel x,y:q*. x E y) & (x,y:q*. Dec(x E y)) (h:(q*q*). (x,y:q*. (x E y) h(x) = h(y)) & (x:q*. x E (h(x))))

About:

1	1. `q:` 2. `0 < q` `E:(qqProp). (EquivRel x,y:q. x E y) & (x,y:q. Dec(x E y)) (h:(qq). (x,y:q. (x E y) h(x) = h(y)) & (x:q. x E (h(x))))`
2	1. `q:` 2. `0 < q` `E:(qqProp). (EquivRel x,y:q. x E y) & (x,y:q. Dec(x E y)) (h:(qq). (x,y:q. (x E y) h(x) = h(y)) & (x:q. x E (h(x))))`