proposition: Theorem Eeq_sym_realizer : forall e, Eeq_sym↓e ⊩ ∀x, ∀y, (x ≡≡ y → y ≡≡ x)%Re.
proof: Proof. intro e. unfold Eeq. start. apply Ht0. repeat split; try ok. start. apply Ht. find. start. apply Ht3. eok. split; ok. start. apply Ht. find. start. apply Ht2. eok. split; ok. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions