fact: Definition safe_finite_subtree (T : 𝒯__f) (π : list index) (H : defined ((proj1_sig (fst (proj1_sig T))) π)) : 𝒯__f := exist _ (pair (exist _ (subtree (proj1_sig (fst (proj1_sig T))) π) (subtree_is_tree_type (fst (proj1_sig T)) π H)) (finite_subtree_domain T π)) (finite_subtree_has_domain T π H).
imports: Coq(Lia Lists.List) Equations(Equations)