PrintForm
Definitions
mb
nat
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
rel
star
weakening
T
:Type,
x
,
y
:
T
,
R
:(
T
T
Prop).
x
=
y
(
x
(
R
^*)
y
)
By:
Auto THEN Unfold `rel_star` 0 THEN Reduce 0 THEN InstConcl [0] THEN ReduceExp 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
mb
nat
Sections
MarkB
generic
Doc
T:Type, x,y:T, R:(T
TProp). x = y 
(x (R^*) y) T:Type, x,y:T, R:(TTProp). x = y (x (R^*) y)
