--- Polymorphic Equality

( EQ : {U | Type} U -> U -> Prop )

--- Symmetric Equality

( SEQ : {U | Type} U -> U -> Prop )

( SEQ_comm : || {U : Type}{x,y : U}(EQ (SEQ x y) (SEQ y x))  )

( SEQ_ax : ?? {U : Type}{x,y : U} (EQ x y) -> (SEQ x y) )

--- Polumorphic Transition Relation

( TR : {EV, ST | Type} EV -> ST -> ST -> Prop )

--- Experimental Subtyping

( ST : Type -> Type -> Prop )

--- ( ST_ax : ?? {U,V : Type} (SEQ U V) -> (ST U V) )

( prop : Type -> Prop )
( prop_ax : {T : Type} T -> (prop T) )
( prop_ax2 : {T : Type} (prop T) -> T )