fact: Definition Req_sym := λ"Eqxy" λ"ε₁" λ"ε₂" λ"q₁" λ"q₂" λ"X" λ"Y" "Eqxy" @ "ε₂" @ "ε₁" @ "q₂" @ "q₁" @ "Y" @ "X".
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions