proposition: Lemma applications_rect: (∀ v a, P (Var v a)) → (∀ o, applications (Op _ o)) → (∀ a (t: Term0 V a), P t).
proof: Proof. intros X0 X1 ??. cut (applications t). intros. assumption. induction t; simpl. apply X0. apply IHt1; exact IHt2. apply X1. Defined.
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.misc.util MathClasses.theory.jections MathClasses.interfaces.ua_basic