proposition: Lemma dumbAbsRel_must_be_nil : forall abs conc, dumbAbsRel abs conc -> conc = nil -> abs = nil.
proof: Proof. unfold dumbAbsRel; simpl; intros. subst. destruct abs; simpl in *; intuition. exfalso; eauto. Qed.
imports: Tutorial