congruence_ax_aux :: Id -> OpType -> CASLFORMULA
congruence_ax_aux name ot = cong_form'
     where OpType _ args res = ot
           free_name = mkFreeName name
           free_args = map mkFreeName args
           free_res = mkFreeName res
           free_ot = Op_type Total free_args free_res nullRange
           free_os = mkQualOp free_name free_ot
           lgth = length free_args
           xs = createVars 1 free_args
           ys = createVars (1 + lgth) free_args
           fst_term = mkAppl free_os xs
           snd_term = mkAppl free_os ys
           phi = phiName res
           pt = Pred_type [free_res, free_res] nullRange
           ps = mkQualPred phi pt
           fst_form = mkPredication ps [fst_term, fst_term]
           snd_form = mkPredication ps [snd_term, snd_term]
           vars_forms = congruence_ax_vars args xs ys
           conj = conjunct $ fst_form : snd_form : vars_forms
           concl = mkPredication ps [fst_term, snd_term]
           cong_form = mkImpl conj concl
           cong_form' = quantifyUniversally cong_form
congruence_ax_aux :: Id -> OpType -> CASLFORMULA
congruence_ax_aux name ot = cong_form'
     where OpType _ args res = ot
           free_name = mkFreeName name
           free_args = map mkFreeName args
           free_res = mkFreeName res
           free_ot = Op_type Total free_args free_res nullRange
           free_os = mkQualOp free_name free_ot
           lgth = length free_args
           xs = createVars 1 free_args
           ys = createVars (1 + lgth) free_args
           fst_term = mkAppl free_os xs
           snd_term = mkAppl free_os ys
           phi = phiName res
           pt = Pred_type [free_res, free_res] nullRange
           ps = mkQualPred phi pt
           fst_form = mkPredication ps [fst_term, fst_term]
           snd_form = mkPredication ps [snd_term, snd_term]
           vars_forms = congruence_ax_vars args xs ys
           conj = conjunct $ fst_form : snd_form : vars_forms
           concl = mkPredication ps [fst_term, snd_term]
           cong_form = mkImpl conj concl
           cong_form' = quantifyUniversally cong_form
congruence_ax_aux name ot = cong_form'
     where OpType _ args res = ot
           free_name = mkFreeName name
           free_args = map mkFreeName args
           free_res = mkFreeName res
           free_ot = Op_type Total free_args free_res nullRange
           free_os = mkQualOp free_name free_ot
           lgth = length free_args
           xs = createVars 1 free_args
           ys = createVars (1 + lgth) free_args
           fst_term = mkAppl free_os xs
           snd_term = mkAppl free_os ys
           phi = phiName res
           pt = Pred_type [free_res, free_res] nullRange
           ps = mkQualPred phi pt
           fst_form = mkPredication ps [fst_term, fst_term]
           snd_form = mkPredication ps [snd_term, snd_term]
           vars_forms = congruence_ax_vars args xs ys
           conj = conjunct $ fst_form : snd_form : vars_forms
           concl = mkPredication ps [fst_term, snd_term]
           cong_form = mkImpl conj concl
           cong_form' = quantifyUniversally cong_form