Library eqSoundness

Require Import soundness.
Require Import evalCompletion.

Soundness for eq evidence

Theorem EQSound : EQSoundness.
unfold EQSoundness.
intros.
induction H.
auto. auto.
symmetry in H1. apply synEq_eq in H1. subst. auto.
subst.
simpl.
rewrite IHEQEvid1. rewrite IHEQEvid2. auto.

Admitted.