ssr_under.out « output « test-suite - coq - The formal proof system

about summary refs log tree commit diff

path: root/test-suite/output/ssr_under.out

blob: 499d25391eb8e968896a5f7afe02612fa09406a9 (plain)

'Under[ m - m ]
(G (fun _ : nat => 0) n >= 0)
'Under[ r = R0 \/ E r ]
(Rbar_le Rbar0 (Lub_Rbar (fun r : R => r = R0 \/ E r)))