Library eqSoundness
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.