
CONTEXT SUMMARY
===============

* Theory: Set is predicative
  
* Axioms:
    ExtractionInCoq.CicMeta.SignCheck.wf_sign_ext_admitted
    ExtractionInCoq.CicMeta.SubtypingDec.unsafe_sn
    ExtractionInCoq.CicMeta.SubtypingDec.unsafe_acc
    ExtractionInCoq.CicMeta.SubtypingDec.subtype_dec_admitted2
    ExtractionInCoq.CicMeta.SubtypingDec.subtype_dec_admitted1
    ExtractionInCoq.CicMeta.SubtypingDec.subtype_dec_admitted0
    ExtractionInCoq.CicMeta.SubtypingDec.subtype_dec_admitted
    ExtractionInCoq.CicMeta.CicPts.par_ctxt_struct
    ExtractionInCoq.CicMeta.MoreCic.gclosed_stable_wctxt
    ExtractionInCoq.CicMeta.MoreCic.fix_types_projn_arg_admitted0
    ExtractionInCoq.CicMeta.MoreCic.fix_types_projn_arg_admitted
    ExtractionInCoq.Extraction.Extraction.extract_term_admitted
    Coq.Logic.Eqdep.Eq_rect_eq.eq_rect_eq
    ExtractionInCoq.Extraction.Extraction.discard_admitted0
    ExtractionInCoq.Extraction.Extraction.discard_admitted
    ExtractionInCoq.CicMeta.InvReduction.confluent_redn
    ExtractionInCoq.CicMeta.InvReduction.commut_alpha_redn
    ExtractionInCoq.CicMeta.InvReduction.commut_alpha_red1
    ExtractionInCoq.CicMeta.MoreCic.closed_stable_wctxt
    ExtractionInCoq.CicMeta.MoreCic.closed_normal_ind_form_admitted9
    ExtractionInCoq.CicMeta.MoreCic.closed_normal_ind_form_admitted8
    ExtractionInCoq.CicMeta.MoreCic.closed_normal_ind_form_admitted7
    ExtractionInCoq.CicMeta.MoreCic.closed_normal_ind_form_admitted6
    ExtractionInCoq.CicMeta.MoreCic.closed_normal_ind_form_admitted5
    ExtractionInCoq.CicMeta.MoreCic.closed_normal_ind_form_admitted4
    ExtractionInCoq.CicMeta.MoreCic.closed_normal_ind_form_admitted3
    ExtractionInCoq.CicMeta.MoreCic.closed_normal_ind_form_admitted2
    ExtractionInCoq.CicMeta.MoreCic.closed_normal_ind_form_admitted19
    ExtractionInCoq.CicMeta.MoreCic.closed_normal_ind_form_admitted18
    ExtractionInCoq.CicMeta.MoreCic.closed_normal_ind_form_admitted17
    ExtractionInCoq.CicMeta.MoreCic.closed_normal_ind_form_admitted16
    ExtractionInCoq.CicMeta.MoreCic.closed_normal_ind_form_admitted15
    ExtractionInCoq.CicMeta.MoreCic.closed_normal_ind_form_admitted14
    ExtractionInCoq.CicMeta.MoreCic.closed_normal_ind_form_admitted13
    ExtractionInCoq.CicMeta.MoreCic.closed_normal_ind_form_admitted12
    ExtractionInCoq.CicMeta.MoreCic.closed_normal_ind_form_admitted11
    ExtractionInCoq.CicMeta.MoreCic.closed_normal_ind_form_admitted10
    ExtractionInCoq.CicMeta.MoreCic.closed_normal_ind_form_admitted1
    ExtractionInCoq.CicMeta.MoreCic.closed_normal_ind_form_admitted0
    ExtractionInCoq.CicMeta.MoreCic.closed_normal_ind_form_admitted
    ExtractionInCoq.CicMeta.MoreCic.closed_ind_form_cstr
    ExtractionInCoq.CicMeta.WfSign.cci_is_strongly_normalizing_axiom
    ExtractionInCoq.Extraction.Relational.Pe_redn_correct_source_admitted9
    ExtractionInCoq.Extraction.Relational.Pe_redn_correct_source_admitted8
    ExtractionInCoq.Extraction.Relational.Pe_redn_correct_source_admitted7
    ExtractionInCoq.Extraction.Relational.Pe_redn_correct_source_admitted6
    ExtractionInCoq.Extraction.Relational.Pe_redn_correct_source_admitted5
    ExtractionInCoq.Extraction.Relational.Pe_redn_correct_source_admitted4
    ExtractionInCoq.Extraction.Relational.Pe_redn_correct_source_admitted3
    ExtractionInCoq.Extraction.Relational.Pe_redn_correct_source_admitted2
    ExtractionInCoq.Extraction.Relational.Pe_redn_correct_source_admitted10
    ExtractionInCoq.Extraction.Relational.Pe_redn_correct_source_admitted1
    ExtractionInCoq.Extraction.Relational.Pe_redn_correct_source_admitted0
    ExtractionInCoq.Extraction.Relational.Pe_redn_correct_source_admitted
    ExtractionInCoq.Extraction.Relational.Pe_redn_correct_admitted3
    ExtractionInCoq.Extraction.Relational.Pe_redn_correct_admitted2
    ExtractionInCoq.Extraction.Relational.Pe_redn_correct_admitted1
    ExtractionInCoq.Extraction.Relational.Pe_redn_correct_admitted0
    ExtractionInCoq.Extraction.Relational.Pe_redn_correct_admitted

