proposition: Lemma nilTerms : forall x : Terms 0, Tnil = x.
proof: Proof. assert (H: forall (n : nat) (p : n = 0) (x : Terms n), nilTermsHelp n p = x). { intros n p x; induction x as [| n t x Hrecx]. - reflexivity. - discriminate p. } replace Tnil with (nilTermsHelp 0 (refl_equal 0)); [apply H | reflexivity]. Qed.
imports: Coq(Lists.List Ensembles Peano_dec Eqdep_dec Arith Compare_dec Utf8) hydras(Ackermann.misc Compat815 )