WhoCites Definitions mb hybrid Sections GenAutomata Doc

Who Cites tr refines?
tr_refinesDef P refines Q == tr:|E| List. P(tr) Q(tr)
Thm* E:Structure, P,Q:((|E| List)Prop). (P refines Q) Prop
carrier Def |S| == 1of(S)
Thm* S:Structure. |S| Type
pi1 Def 1of(t) == t.1
Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A

Syntax:P refines Q has structure: tr_refines(E; P; Q)

About:
spreadproductlistapplyfunctionuniverse
memberpropimpliesall!abstraction

WhoCites Definitions mb hybrid Sections GenAutomata Doc