proposition: Theorem termInd_ind : ind lowP e_s = term_ind P R.
proof: Proof. rewrite invind. unfold ind_weq. simpl. rewrite inv_weqonsec. rewrite inv_weqonsec. use maponpaths. apply idpath. Defined.
imports: UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Induction.PolynomialFunctors UniMath.Induction.W.Core UniMath.Induction.W.Wtypes UniMath.Induction.FunctorAlgebras_legacy UniMath.Algebra.Universal.Signatures UniMath.Algebra.Universal.Algebras UniMath.Algebra.Universal.HVectors UniMath.Algebra.Universal.Terms