proposition: Lemma subst_subst k u t : subst_term k u t = subst_term k u t.
proof: Proof. revert k u t. refine (fst (subst_term_elim (fun k u t c => c = c) (fun k u l c => c = c) _ _ _ _ _ _)); trivial. Qed.
imports: Equations(Equations) Program Arith List Compare_dec