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