Thms automata 4 Sections AutomataTheory Doc

NOTE: Refl(A)(R(_1;_2)) is alpha-equivalent to Refl(A;x,y.R(x;y)).

refl Def Refl(T;x,y.E(x;y)) == a:T. E(a;a)

Thm* T:Type, E:(TTProp). Refl(T;x,y.E(x,y)) Prop

About:
!abstractionalluniversefunctionpropmember