WhoCites Definitions mb hybrid Sections GenAutomata Doc

Who Cites preserved by2?
preserved_by2Def (ternary) R preserves P == x,y,z:T. P(x) P(y) R(x,y,z) P(z)
Thm* T:Type, P:(TProp), R:(TTTProp). (ternary) R preserves P Prop

Syntax:(ternary) R preserves P has structure: preserved_by2(T; R; P)

About:
applyfunctionuniversememberpropimpliesall!abstraction

WhoCites Definitions mb hybrid Sections GenAutomata Doc