proposition: Lemma absRel_reversed_rep : forall abs conc r, absRel abs conc -> fst conc = nil -> snd conc <> nil -> r = rev (snd conc) -> absRel (tl abs) (tl r, nil).
proof: Proof. unfold absRel; intuition simpl in *; subst. autorewrite with core; auto. Qed.
imports: Tutorial