P1 ≟ refl ? (eq0 (LIST S)),
P2 ≟ sym ? (eq0 (LIST S)),
P3 ≟ trans ? (eq0 (LIST S)),
P1 ≟ refl ? (eq0 (LIST S)),
P2 ≟ sym ? (eq0 (LIST S)),
P3 ≟ trans ? (eq0 (LIST S)),
-unification hint 0 ≔ S:setoid, A,B:list S;
- MM ≟ mk_unary_morphism ??
- (λA:list S.mk_unary_morphism ?? (λB:list S.A @ B) (prop1 ?? (append_is_morph S A)))
+unification hint 0 ≔ S:setoid, A,B:list (carr S);
+ SS ≟ carr S,
+ MM ≟ mk_unary_morphism ?? (λA:list (carr S).
+ mk_unary_morphism ??
+ (λB:list (carr S).A @ B) (prop1 ?? (fun1 ??(append_is_morph S) A)))
(prop1 ?? (append_is_morph S)),
T ≟ LIST S
(*--------------------------------------------------------------------------*) ⊢
(prop1 ?? (append_is_morph S)),
T ≟ LIST S
(*--------------------------------------------------------------------------*) ⊢