/root/interactive/lean/phase6/Family.lean:316:9: warning: unused variable `i`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
'NimAudit.Family.polyIn_const' depends on axioms: [propext]
'NimAudit.Family.polyIn_leaf' depends on axioms: [propext]
'NimAudit.Family.polyIn_add' depends on axioms: [propext, Quot.sound]
'NimAudit.Family.polyIn_mul' depends on axioms: [propext]
'NimAudit.Family.polyIn_pow' depends on axioms: [propext]
'NimAudit.Family.polyIn_mono' does not depend on any axioms
'NimAudit.Family.PE.poly' depends on axioms: [propext, Quot.sound]
'NimAudit.Family.length_le_tsize' depends on axioms: [propext, Quot.sound]
'NimAudit.Family.AC0Fam.outs_poly' depends on axioms: [propext, Quot.sound]
'NimAudit.Family.netBounded_mono' does not depend on any axioms
'NimAudit.Family.netFam_ac0' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Family.log2_lt_self' depends on axioms: [propext, Quot.sound]
'NimAudit.Family.rIdx_le' depends on axioms: [propext, Quot.sound]
'NimAudit.Family.rIdx_width' depends on axioms: [propext]
'NimAudit.Family.rIdx_counter' depends on axioms: [propext]
'NimAudit.Family.tsize_bForms' depends on axioms: [propext, Quot.sound]
'NimAudit.Family.bForms_mem' depends on axioms: [propext, Quot.sound]
'NimAudit.Family.bin_cert' depends on axioms: [propext, Quot.sound]
'NimAudit.Family.wired_mono' does not depend on any axioms
'NimAudit.Family.binNet_cert' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Family.polyE' depends on axioms: [propext, Quot.sound]
'NimAudit.Family.restLen_pos' depends on axioms: [propext, Quot.sound]
'NimAudit.Family.rest_B' depends on axioms: [propext, Quot.sound]
'NimAudit.Family.rest_N' depends on axioms: [propext, Quot.sound]
'NimAudit.Family.rest_leaves' depends on axioms: [propext, Quot.sound]
'NimAudit.Family.rest_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Family.rest_sizePoly' depends on axioms: [propext, Quot.sound]
'NimAudit.Family.rest_ac0' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Family.rest_net' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Family.rest_semantics' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Family.polLen_pos' does not depend on any axioms
'NimAudit.Family.pol_B' depends on axioms: [propext]
'NimAudit.Family.pol_N' depends on axioms: [propext]
'NimAudit.Family.pol_leaves' depends on axioms: [propext, Quot.sound]
'NimAudit.Family.pol_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Family.pol_sizePoly' depends on axioms: [propext, Quot.sound]
'NimAudit.Family.pol_ac0' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Family.pol_net' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Family.pol_semantics' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Family.mhLen_pos' depends on axioms: [propext, Quot.sound]
'NimAudit.Family.mh_B' depends on axioms: [propext, Quot.sound]
'NimAudit.Family.mh_N' depends on axioms: [propext, Quot.sound]
'NimAudit.Family.mh_leaves' depends on axioms: [propext, Quot.sound]
'NimAudit.Family.mh_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Family.mh_sizePoly' depends on axioms: [propext, Quot.sound]
'NimAudit.Family.mh_ac0' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Family.mh_net' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Family.mh_semantics' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Family.ctrl_widths' depends on axioms: [propext, Quot.sound]
'NimAudit.Family.ctrlLen_pos' depends on axioms: [propext, Quot.sound]
'NimAudit.Family.ctrl_leaves' depends on axioms: [propext, Quot.sound]
'NimAudit.Family.ctrl_ac0' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Family.ctrl_net' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Family.ctrl_semantics' depends on axioms: [propext, Classical.choice, Quot.sound]