P1 ≟ refl ? (eq0 (LIST S)),
P2 ≟ sym ? (eq0 (LIST S)),
P3 ≟ trans ? (eq0 (LIST S)),
- X ≟ mk_setoid (list S) (mk_equivalence_relation ? (eq_list T) P1 P2 P3)
+ X ≟ mk_setoid (list (carr S)) (mk_equivalence_relation ? (eq_list S) P1 P2 P3)
(*-----------------------------------------------------------------------*) ⊢
carr X ≡ list T.
-unification hint 0 ≔ S:setoid,a,b:list S;
+unification hint 0 ≔ S:setoid, a,b:list (carr S);
R ≟ eq0 (LIST S),
- L ≟ (list S)
+ L ≟ (list (carr S))
(* -------------------------------------------- *) ⊢
eq_list S a b ≡ eq_rel L R a b.
nqed.
alias symbol "hint_decl" (instance 1) = "hint_decl_Type0".
-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
(*--------------------------------------------------------------------------*) ⊢
- fun1 T T (fun1 T (unary_morph_setoid T T) MM A) B ≡ A @ B.
+ fun1 T T (fun1 T (unary_morph_setoid T T) MM A) B ≡ append SS A B.
(* XXX to understand if are always needed or only if the coercion is active *)