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