Объединение деревьев вместе для создания нового дерева — Coq

Я пытаюсь создать новую модель счетчика на основе списка предыдущих моделей счетчиков. Эти модели структурированы как деревья. В настоящее время я смотрю только на отношение достижимости. Пример: Для модели с корневым миром w и отношением достижимости R пусть new_R := RU (u,w) Это создает новую модель с корневым миром u и отношением достижимости new_R.

Чтобы создать отношение достижимости, я описал функцию, которая говорит: Любые два мира u,w; (u,w) в new_R, если:

1. ЕСЛИ u — это новый_корень, ТО w должен быть корнем последующей модели. И
2. ЕСЛИ w — это new_root, ТО u должен быть корнем предшествующей модели. И
3. ЕСЛИ (u!=корень и w!=корень), ТО существует R в списке моделей, таких что (R u w). Я попытался закодировать его следующим образом:

Definition join_rel (world : Type)
  (ws_bac : list(world)) (rs_bac : list(world -> world -> Prop))
  (ws_fwd : list(world)) (rs_fwd : list(world -> world -> Prop))
  (w : world) : world -> world -> Prop :=
(fun w1 w2 => (w1 = w -> In w2 ws_fwd) /\
              (w2 = w -> In w1 ws_bac) /\
              ((~w1 = w /\ ~w2 = w) ->
               (exists w' r',  (* <w,R> *)
                 (In (w',r') (combine (ws_fwd++ws_bac) (rs_fwd ++ rs_bac)) /\
                  reachable r' w1 w' /\ reachable r' w2 w' /\ r' w1 w2)))).

По сути, первое предложение связывает мой новый корень со всеми моделями, которые должны быть преемниками. Второй пункт соединяет мой новый корень со всеми предшественниками. Третий пункт копирует информацию из предыдущих моделей. Этот пункт создает мне проблемы, и я считаю, что эта формализация слишком проста.

Пусть R_new будет новым отношением, которое мы получим, взяв объединение, как описано выше. Пусть R1 — отношение для модели M1 с корнем w1. Я хочу доказать, что: Для всех миров (w) в M1, если R_new w w1, то R1 w w1.

Причина, по которой должно пройти доказательство, следующая:

1. Поскольку w находится в M1, следовательно, w не является новым корнем. Поскольку w1 является корнем, другая модель, следовательно, w1 не является новым_корнем. Итак, рассматриваем пункт 3.
2. Существует такое R, что R w w1. Так как w находится в M1, R должно быть R1.
3. Поэтому R1 w w1.

Однако мой текущий подход слишком слаб, чтобы доказать это. У меня проблема с пунктом 2. Кто-нибудь знает, как это формализовать? Coq жалуется, что R не обязательно должен быть R1. Моя текущая идея состоит в том, чтобы каждый отдельный R использовал отдельный тип, так что R1 : world1 -> world1 -> Prop; R2 : world2 -> world2 -> Prop и т. д. Однако затем я изо всех сил пытаюсь написать функцию соединения, так как я даже не знаю, с чего начать с этим подходом.

Любой совет будет полезен. Я новичок в Coq, поэтому ссылки, где я могу прочитать о похожих проблемах, тоже были бы кстати.