proposition: Lemma eta_abs_snd : forall abs conc, absRel abs conc -> snd conc <> nil -> abs = hd dummy abs :: tl abs.
proof: Proof. unfold absRel; destruct abs; simpl; intros. destruct (snd conc); simpl in *; intuition. apply (f_equal (@length _)) in H. repeat rewrite app_length in H; simpl in H. arithmetic. auto. Qed.
imports: Tutorial