proposition: Lemma absRel_fast_rep : forall abs conc, absRel abs conc -> fst conc <> nil -> absRel (tl abs) (tl (fst conc), snd conc).
proof: Proof. unfold absRel; intuition simpl in *; subst. destruct (fst conc); simpl in *; tauto. Qed.
imports: Tutorial