proposition: Lemma dumbAbsRel_pop_rep : forall abs conc r, dumbAbsRel abs conc -> conc <> nil -> r = getLast conc -> dumbAbsRel (tl abs) (fst r).
proof: Proof. unfold dumbAbsRel; intros; subst. destruct abs; simpl in *; intuition. apply getLast_append_list. Qed.
imports: Tutorial