proposition: Lemma nqe_always {t} (term: Term _ nat t) vars: nqe (eval et vars term) (λ i, eval et (λ sort n, vars sort n i) term).
proof: Proof. induction term; simpl in *. reflexivity. set (k := (λ i : I, eval et (λ (sort: sorts et) (n : nat), vars sort n i) term1 (eval et vars term2 i))). cut (nqe (eval et vars term1 (eval et vars term2)) k). set (p := λ i : I, eval et (λ (sort : sorts et) (n : nat), vars sort n i) term1 (eval et (λ (sort : sorts et) (n : nat), vars sort n i) term2)). assert (op_type_equiv (sorts et) carrier t (eval et vars term1 (eval et vars term2)) (eval et vars term1 (eval et vars term2))). apply sig_type_refl. intro. apply _. apply eval_proper; try apply _. reflexivity. reflexivity. apply (nqe_proper t (eval et vars term1 (eval et vars term2)) (eval et vars term1 (eval et vars term2)) H2 k p). subst p k. simpl. intro. pose proof (eval_proper et _ (λ (sort : sorts et) (n : nat), vars sort n i) (λ (sort : sorts et) (n : nat), vars sort n i) (reflexivity _) term1 term1 eq_refl). apply H3. apply IHterm2. apply IHterm1. change (nqe (rec_impl et _ _ (et o) (λ i : I, @algebra_op _ (carriers i) _ o)) (λ i : I, @algebra_op _ (carriers i) _ o)). generalize (λ i: I, @algebra_op et (carriers i) _ o). induction (et o); simpl. reflexivity. intros. apply IHo0. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.theory.categories MathClasses.categories.varieties