- us_unifbase: (us_carr square → Prop) → CProp;
- us_phi1: ∀U:us_carr square → Prop. us_unifbase U →
- (λx:us_carr square.\fst x ≈ \snd x) ⊆ U;
- us_phi2: ∀U,V:us_carr square → Prop. us_unifbase U → us_unifbase V →
- ∃W:us_carr square → Prop.us_unifbase W ∧ (W ⊆ (λx.U x ∧ V x));
- us_phi3: ∀U:us_carr square → Prop. us_unifbase U →
- ∃W:us_carr square → Prop.us_unifbase W ∧ (W ∘ W) ⊆ U;
- us_phi4: ∀U:us_carr square → Prop. us_unifbase U → ∀x.(U x → (inv U) x) ∧ ((inv U) x → U x)
+ us_unifbase: (us_carr squareB → Prop) → CProp;
+ us_phi1: ∀U:us_carr squareB → Prop. us_unifbase U →
+ (λx:us_carr squareB.\fst x ≈ \snd x) ⊆ U;
+ us_phi2: ∀U,V:us_carr squareB → Prop. us_unifbase U → us_unifbase V →
+ ∃W:us_carr squareB → Prop.us_unifbase W ∧ (W ⊆ (λx.U x ∧ V x));
+ us_phi3: ∀U:us_carr squareB → Prop. us_unifbase U →
+ ∃W:us_carr squareB → Prop.us_unifbase W ∧ (W ∘ W) ⊆ U;
+ us_phi4: ∀U:us_carr squareB → Prop. us_unifbase U → ∀x.(U x → (\inv U) x) ∧ ((\inv U) x → U x)