fact: Definition lambda_calculus_ind {L : lambda_calculus_data} (A : ∏ n (l : L n), hSet) (f_var : ∏ n i, A n (var i)) (f_app : ∏ n l l', A _ l → A _ l' → A n (app l l')) (f_abs : ∏ n l, A _ l → A n (abs l)) (f_subst : ∏ m n l f, A m l → (∏ i, A _ (f i)) → A n (subst l f)) (f_inflate := (λ n _ al, f_subst _ _ _ _ al (λ i, (f_var _ (stnweq (inl i))))) : ∏ n (l : L n), A n l → A (S n) (inflate l)) (f_paths : (∏ m n i f af, PathOver (Y := A n) (subst_var i f) (f_subst _ _ _ _ (f_var m i) af) (af i)) × (∏ m n l al l' al' f af, PathOver (Y := A n) (subst_app l l' f) (f_subst _ _ _ _ (f_app m _ _ al al') af) (f_app _ _ _ (f_subst _ _ _ _ al af) (f_subst _ _ _ _ al' af))) × (∏ m n l al f af, PathOver (Y := A n) (subst_abs l f) (f_subst _ _ _ _ (f_abs m _ al) af) (f_abs _ _ (f_subst _ _ _ _ al (extend_tuple_dep (A := A (S n)) (λ i, f_inflate _ _ (af i)) (f_var _ (stnweq (inr tt))))))) × (∏ l m n t a g ag f af, PathOver (Y := A n) (subst_subst t g f) (f_subst m n _ _ (f_subst l m _ _ a ag) af) (f_subst _ _ _ _ a (λ i, f_subst _ _ _ _ (ag i) af))) × (∏ n f af g ag, PathOver (Y := A n) (beta_equality f g) (f_app _ _ _ (f_abs _ _ af) ag) (f_subst _ _ _ _ af (extend_tuple_dep (A := A n) (f_var _) ag))) ) : (∏ n l, A n l) := pr2 (pr222 (pr222 (pr222 L))) A f_var f_app f_abs f_subst (pr1 f_paths) (pr12 f_paths) (pr122 f_paths) (pr1 (pr222 f_paths)) (pr2 (pr222 f_paths)).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Tuples