(10steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

At: closed rel mng sq

r:rel(), rho,ds,da1,da2,de,s,e,a1,a2,tr:Top. closed_rel(r) ([[r]] rho ds da1 de e s a1 tr ~ [[r]] rho ds da2 de e s a2 tr)
By: UnivCD
Generated subgoal:

11. r: rel()
2. rho: Top
3. ds: Top
4. da1: Top
5. da2: Top
6. de: Top
7. s: Top
8. e: Top
9. a1: Top
10. a2: Top
11. tr: Top
12. closed_rel(r)
[[r]] rho ds da1 de e s a1 tr ~ [[r]] rho ds da2 de e s a2 tr

About:
sqequaltopimpliesall

(10steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc