proposition: Lemma dumbAbsRel_pop_data : forall abs conc r, dumbAbsRel abs conc -> conc <> nil -> r = getLast conc -> hd dummy abs = snd r.
proof: Proof. unfold dumbAbsRel; intros; subst. destruct abs; simpl in *; intuition. rewrite getLast_append_data; auto. Qed.
imports: Tutorial