- let dno, ae = match get_inner_types st t with
- | None -> false, true
- | Some (sty, ety) ->
- let sty, ety = H.cic sty, H.cic ety in
- DTI.does_not_occur 1 sty && DTI.does_not_occur 1 ety,
- Ut.alpha_equivalence sty ety
- in
- let dno = dno && DTI.does_not_occur 1 (H.cic t) in
- let name = match dno, name with
- | true, _ -> C.Anonymous
- | false, C.Anonymous -> H.mk_fresh_name st.context used_premise
- | false, name -> name