proposition: Theorem parse_rel_fun : forall l l1 t1, parse_rel l l1 t1 -> forall l2 t2, parse_rel l l2 t2 -> l1 = l2.
proof: Proof. intros l l1 t1 Hp1; elim Hp1. - intros l2 l3 l4 t2 t3 Hp2 Hrec2 Hp3 Hrec3 l5 t4 H'. inversion H'. match goal with Hid : parse_rel l2 (close:: _) _ |- _ => generalize (Hrec2 _ _ Hid) end. intros heq1; injection heq1. intros heq2; subst l3. eapply Hrec3; eauto. - intros l2 t2 Hp2; inversion Hp2; trivial. - intros l0 l2 t2 Hp2; inversion Hp2; trivial. Qed.
imports: Arith Lia List Wellfounded parsing