Nuprl - Pf assert_st

s1,s2:SimpleType. st_eq(s1;s2) s1 = s2

By: Auto

Generated subgoals:

1 1. s1: SimpleType
2. s2: SimpleType
3. st_eq(s1;s2)
s1 = s2

2 1. s1: SimpleType
2. s2: SimpleType
3. s1 = s2
st_eq(s1;s2)

About:

1	1. `s1:` `SimpleType` 2. `s2:` `SimpleType` 3. `st_eq(s1;s2)` `s1 = s2`
2	1. `s1:` `SimpleType` 2. `s2:` `SimpleType` 3. `s1 = s2` `st_eq(s1;s2)`