proposition: Lemma consTerms : forall (n : nat) (x : Terms (S n)), {t : Term * Terms n | Tcons n (fst t) (snd t) = x}.
proof: Proof. assert (H: forall (n : nat) (x : Terms n), consTermsHelp n x). { intros n x; induction x as [| n t x Hrecx]. - simpl in |- *; intros p; exists tt. elim p using K_dec_set. + apply eq_nat_dec. + reflexivity. - simpl in |- *; intro p; exists (t, x). elim p using K_dec_set. + apply eq_nat_dec. + simpl in |- *; reflexivity. } intros n x; assert (H0: consTermsHelp _ x) by apply H. simpl in H0; apply (H0 (refl_equal (S n))). Qed.
imports: Coq(Lists.List Ensembles Peano_dec Eqdep_dec Arith Compare_dec Utf8) hydras(Ackermann.misc Compat815 )