UniAna.testtac.TestTac

Require Import Evaluation.

Section test_spot_path.

  Context `{redCFG}.

(*  Goal forall t, EPath' t -> CPath' (ne_map fst (ne_map fst t)).  intros. spot_path. Qed.
  Goal forall t, Tr t -> CPath' (ne_map fst (ne_map fst t)).  intros.  spot_path. Qed.*)

End test_spot_path.