fact: Definition lambda_calculus_rect {L : lambda_calculus_data} (A : nat → hSet) (f_var : ∏ n, stn n → A n) (f_app : ∏ n, A n → A n → A n) (f_abs : ∏ n, A (S n) → A n) (f_subst : ∏ m n, A m → (stn m → A n) → A n) (f_inflate := (λ n a, f_subst _ _ a (λ i, (f_var _ (stnweq (inl i))))) : ∏ n, A n → A (S n)) (f_paths : (∏ m n i af, (f_subst m n (f_var m i) af) = (af i)) × (∏ m n al al' af, (f_subst m n (f_app _ al al') af) = (f_app _ (f_subst _ _ al af) (f_subst _ _ al' af))) × (∏ m n al af, (f_subst m n (f_abs m al) af) = (f_abs _ (f_subst _ _ al (extend_tuple (λ i, f_inflate _ (af i)) (f_var _ (stnweq (inr tt))))))) × (∏ l m n a ag af, (f_subst m n (f_subst l m a ag) af) = (f_subst _ _ a (λ i, f_subst _ _ (ag i) af))) × (∏ n af ag, (f_app n (f_abs _ af) ag) = (f_subst _ _ af (extend_tuple (f_var _) ag))) ) : (∏ n, L n → A n).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Tuples