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