(*
A nu-tree can have nu nodes in addition to the usual tree construction.
Nu nodes have a name and a subtree.
*)
Inductive NuTree : Type :=
| Tr : Name -> list NuTree -> NuTree
| Nu : Name -> NuTree -> NuTree.
Implicit Type n nt : NuTree.
(*
A default nu-tree used for nth
*)
Definition DNT :=
Tr (O, O) nil.
Inductive Ntwr : NuTree -> Prop :=
| ntwrA a l : (forall x, x el l -> Ntwr x) -> (rk a) = |l| -> Ntwr (Tr a l)
| ntwrB a x : Ntwr x -> Ntwr (Nu a x).
Lemma nt_wr_sub a l :
Ntwr (Tr a l) -> forall n, n el l -> Ntwr n.
Proof.
inversion 1. intros. auto.
Qed.
Lemma nt_wr_sub' a n :
Ntwr (Nu a n) -> Ntwr n.
Proof.
now inversion 1.
Qed.
(*
Two tactics used to solve proof obligations for wellrankedness
*)
Ltac solve_len :=
repeat match goal with
| [ H : context [?k < length ?l] |- ?k < length ?l ] => assumption
| [ H1 : context [?k < length ?l], H2 : context [ length ?l = length ?l' ] |- ?k < length ?l' ] => now rewrite <-H2
| [ H1 : context [?k < length (map ?f ?l)] |- _ ] => rewrite map_length in H1
| [ |- ?k < length (map ?f ?l) ] => rewrite map_length
| [ |- ?k < length ?l' ] => try congruence
end.
Ltac solve_wr_sub :=
match goal with
| [ H : context [Ntwr (Tr ?a ?l)] |- Ntwr (nth ?k ?l ?m) ] => apply (nt_wr_sub H), nth_In; solve_len
| [ H : context [Ntwr (Nu ?a ?n)] |- Ntwr ?n ] => apply (nt_wr_sub' H); solve_len
| [ H : context [Twr (TrA ?a ?l)] |- Twr (nth ?k ?l ?m) ] => apply (tree_wr_sub H), nth_In; solve_len
| [ H : context [ forall x, x el ?l -> Ntwr x] |- Ntwr (nth ?k ?l ?m) ] => apply H, nth_In; solve_len
| [ H : context [ forall x, x el ?l -> Twr x ] |- Twr (nth ?k ?l ?m) ] => apply H, nth_In; solve_len
end.
Section Depth.
(*
We later define a procedure on nu-trees which is not structurally recursive.
We define the depth of a nu-tree here to enable using it as a termination parameter.
*)
Implicit Type nl : list NuTree.
Fixpoint nt_depth n : nat :=
match n with
| Tr a l => S (list_max (map nt_depth l))
| Nu a n' => S (nt_depth n')
end.
Lemma gt_depth_sub nl k d :
k < |nl| -> d >= (list_max (map nt_depth nl)) -> d >= nt_depth (nth k nl DNT).
Proof.
intros H1 H2. enough(nt_depth(nth k nl DNT) <= list_max (map nt_depth nl)) by omega.
apply list_max_max, in_map_iff. exists (nth k nl DNT).
split; auto using nth_In.
Qed.
Lemma nt_decrease a nl n :
n el nl -> nt_depth n < nt_depth (Tr a nl).
Proof.
intros H1. simpl.
assert(nt_depth n <= (list_max (map nt_depth nl))) by (apply list_max_max, in_map_iff; eauto).
omega.
Qed.
Lemma nt_decrease' a n :
nt_depth n < nt_depth (Nu a n).
Proof.
simpl. auto.
Qed.
Lemma ntd_S n :
nt_depth n <> 0.
Proof.
destruct n; simpl; auto.
Qed.
Lemma ntd_S' n :
nt_depth n > 0.
Proof.
destruct n; simpl; omega.
Qed.
End Depth.
Fixpoint nt_names n : list Name :=
match n with
| Tr a l => a :: (concat (map nt_names l))
| Nu a x => a :: nt_names x
end.
Lemma nt_name_in_sub a n a' l:
a el (nt_names n) -> n el l -> a el (nt_names (Tr a' l)).
Proof.
intros H1 H2. simpl. right. apply concat_map_el.
exists n. now split.
Qed.
(*
There is no empty tree
*)
Fact nt_names_inhab nt :
exists a, a el (nt_names nt).
Proof.
destruct nt; simpl; eauto.
Qed.
Fixpoint BN n : list Name :=
match n with
| Tr a l => concat (map BN l)
| Nu a x => a :: (BN x)
end.
Lemma BN_in_sub a n b l:
a el (BN n) -> n el l -> a el (BN (Tr b l)).
Proof.
intros H1 H2. simpl. apply concat_map_el. now exists n.
Qed.
Lemma bound_in_names n :
Ntwr n -> (BN n) <<= (nt_names n).
Proof.
induction 1 as [a' l H3 H4 _| a' x H3 H4]; simpl.
- apply incl_cons, concat_incl_list, H4.
- intros a [<-|]; auto.
Qed.
Fixpoint FN n :=
match n with
| Tr a l => a :: (concat (map FN l))
| Nu a x => rem (FN x) a
end.
Lemma FN_in_sub a n l b :
a el (FN n) -> n el l -> a el (FN (Tr b l)).
Proof.
intros H1 H2. simpl. right. apply concat_map_el. now exists n.
Qed.
Lemma free_in_names n :
Ntwr n -> (FN n) <<= (nt_names n).
Proof.
induction 1 as [a' l H3 H4 _| a' x H3 H4]; simpl.
- apply incl_shift, concat_incl_list, H4.
- intros a [H5 H6] % in_rem_iff. auto.
Qed.
Lemma tree_name_free a l :
a el FN (Tr a l).
Proof. simpl. now left. Qed.
Lemma free_sub_not a n :
Ntwr n -> ~a el nt_names n -> ~a el FN n.
Proof.
intros HW1 H1 H2 % free_in_names; auto.
Qed.
(*
A name that was free, but isn't free after adding a binding
is equal to the name that was bound.
*)
Lemma bind_free_name b a n :
b el FN n -> ~ b el FN (Nu a n) -> b = a.
Proof.
simpl. intros H1 H2. rewrite in_rem_iff in H2.
intuition. decide(b=a) as [|]; tauto.
Qed.
(*
Inductive predicate for nu-trees without any nus
*)
Inductive NoNus : NuTree -> Prop :=
nonusA a l : (forall x, x el l -> (NoNus x)) -> NoNus (Tr a l).
Fact BN_no_nus n :
Ntwr n -> (BN n = [] <-> NoNus n).
Proof.
intros H1. split.
- induction H1; simpl; auto.
+ rewrite concat_nil'. intros H2. constructor. intros n H3. apply H0; trivial.
apply H2, in_map_iff. eauto.
+ inversion 1.
- induction 1. simpl. rewrite concat_nil'. intros la [n [H2 H3]] % in_map_iff. rewrite <-H2.
inversion H1. subst. apply H0; auto.
Qed.
(*
Inductive predicate for nu-trees without any nus of given rank
*)
Inductive NoNusk (k : nat) : NuTree -> Prop :=
| nonuskA a l : (forall x, x el l -> (NoNusk k x)) -> NoNusk k (Tr a l)
| nonuskB a n : NoNusk k n -> rk a <> k -> NoNusk k (Nu a n).
Fact BN_no_nusk n k :
Ntwr n -> ((forall a, a el BN n -> rk a <> k) <-> NoNusk k n).
Proof.
intros H1. split.
- induction H1 as [a l H1 H2 H3| a n H1 H2]; simpl in *; auto.
+ intros H4. constructor. intros n H5. apply H2; trivial.
intros b H6. apply H4, (BN_in_sub a H6), H5.
+ intros H3. constructor.
* apply H2. intros b H4. apply H3. now right.
* apply H3. now left.
- induction 1 as [a l H2 H3| a n H2 H3 H4]; simpl; intros b; inversion H1; subst.
+ intros [n [H6 H7]] % concat_map_el. apply (H3 n H6); auto.
+ intros [|]; try now subst. apply H3; auto.
Qed.
Fixpoint nt_apply_perm p n :=
match n with
| Tr a l => Tr (p a) (map (nt_apply_perm p) l)
| Nu a x => Nu (p a) (nt_apply_perm p x)
end.
Notation "p *' n" := (nt_apply_perm p n) (at level 45).
Lemma nt_apply_perm_step p a l :
Tr (p a) (map (nt_apply_perm p) l) = p *' (Tr a l).
Proof. reflexivity. Qed.
Section NtAction.
Variable n : NuTree.
Hypothesis HW : Ntwr n.
Lemma nt_assoc p p' :
(p ** p') *' n = (p *' (p' *' n)).
Proof.
induction HW as [a l H1 H2 _ | a x H1 H2]; simpl; f_equal; auto.
rewrite map_map, map_ext_in with (g := (fun n => p *' (p' *' n))); auto.
Qed.
Lemma nt_id :
id *' n = n.
Proof.
induction HW as [a l H1 H2 _ | a x H1 H2]; simpl; f_equal; auto.
rewrite map_ext_in with (g := (fun x => x)); auto using map_id.
Qed.
(*
( *' ) is a sym action for NuTree.
*)
Fact nt_sym :
id *' n = n /\ forall p q, (p ** q) *' n = (p *' (q *' n)).
Proof.
split.
- apply nt_id.
- intros. apply nt_assoc.
Qed.
(*
Lemma about applying a permutation and its inverse to a nu-tree
*)
Lemma nt_perm_apply_inv p p' :
Inv p p' -> n = (p *' (p' *' n)).
Proof.
induction HW as [a l H1 H2 H3| a x H1 H2]; intros H4; simpl.
- assert(HP2: Inv p p') by assumption. specialize (H4 a) as [H4 ->].
rewrite map_map, map_ext_in with (g := fun x => x); try now rewrite map_id.
intros n H5. rewrite <-(H2 n); auto.
- assert(HP2: Inv p p') by assumption. specialize (H4 a) as [H4 ->].
rewrite <-H2; auto.
Qed.
Fact nt_perm_wr p :
Perm p -> Ntwr (p *' n).
Proof.
induction HW as [a l H1 H2 H3 | a x H1 H2]; intros HP; simpl; constructor; auto.
- intros s [s'[<- H7]] % in_map_iff. apply H2; auto.
- destruct HP as [H4 _]. now rewrite map_length, <- H4.
Qed.
Lemma nt_depth_perm p :
nt_depth n = nt_depth (p *' n).
Proof.
induction HW as [a l H1 H2 H3| a' n H1 H2]; simpl; f_equal; auto. f_equal.
rewrite map_map, map_ext_in with (g := fun n => nt_depth (p*'n)); auto.
Qed.
Lemma nt_swap_perm p p' :
(forall a, p a = p' a) -> p *' n = (p' *' n).
Proof.
intros H2. induction HW as [a l H3 H4 _ | a n H3 H4]; simpl; rewrite (H2 a); f_equal; auto.
apply map_ext_in. auto.
Qed.
(*
Stronger version than above, names not in the tree don't matter
With this lemma we get nominality.
*)
Lemma nt_swap_perm' p p' :
(forall a, a el nt_names n -> p a = p' a) -> p *' n = (p' *' n).
Proof.
intros H2. induction HW as [a l H3 H4 _ | a n H3 H4]; simpl; rewrite <-(H2 a); simpl; auto; f_equal.
- apply map_ext_in. intros n H5. apply H4; auto.
intros b H6. apply H2, (nt_name_in_sub a H6 H5).
- rewrite H4; auto. intros b H5. apply H2. simpl. auto.
Qed.
(*
This case occurs frequently.
*)
Lemma nt_swap_perm'' p p' p'' :
(forall a, a el nt_names n -> (p ** p') a = p'' a) -> p *' (p' *' n) = (p'' *' n).
Proof.
intros H1. rewrite <-nt_assoc. now apply nt_swap_perm'.
Qed.
(*
Nu-trees are nominal
*)
Fact nt_nominal p :
(forall x, x el nt_names n -> p x = x) -> p *' n = n.
Proof.
intros H2. rewrite nt_swap_perm' with (p' := id); trivial. exact (nt_id).
Qed.
Lemma nt_assoc3 p1 p2 p3 :
(p1 ** (p2 ** p3) *' n) = (p1 ** p2 ** p3 *' n).
Proof.
now apply nt_swap_perm; trivial.
Qed.
End NtAction.
Section Equivariance.
Variable n : NuTree.
Variable p : NameF.
Hypothesis HW : Ntwr n.
(*
The functions we have defined for nu-trees are all equivariant.
*)
Lemma nt_names_equiv :
nt_names (p *' n) = (p *- (nt_names n)).
Proof.
induction HW as [a l H3 H4 H5| a n t H1]; simpl; try now rewrite H1.
unfold perm_list. rewrite concat_map, map_map, map_map. f_equal. f_equal.
apply map_ext_in. intros. apply H4; auto.
Qed.
Lemma BN_equiv :
p *- (BN n) = BN (p *' n).
Proof.
induction HW as [a l H3 H4 H5| a n t H1]; simpl; try now rewrite H1.
unfold perm_list. rewrite concat_map, map_map, map_map. f_equal. apply map_ext_in.
intros. apply H4; auto.
Qed.
Lemma rem_equiv (a : Name) (l : list Name) :
Perm p -> p *- (rem l a) = rem (p *- l) (p a) .
Proof.
intros HP. induction l as [ | b l IH]; simpl; trivial. decide (p b = p a) as [E1|E1].
- rewrite perm_inj in E1; try assumption. subst. now rewrite rem_fst, rem_fst, <-IH.
- rewrite rem_fst', rem_fst', <-IH; auto. now rewrite <-perm_inj with (p:= p).
Qed.
Lemma rem_equiv' (a b : Name) (l : list Name) :
Perm p -> b = p a -> p *- (rem l a) = rem (p *- l) b.
Proof.
intros H1 H2. subst b. now apply rem_equiv.
Qed.
Lemma FN_equiv :
Perm p -> FN (p *' n) = (p *- FN n).
Proof.
intros H1. induction HW as [a l H2 H3 H4| a n' H2 H3]; simpl.
- unfold perm_list. rewrite concat_map, map_map, map_map. f_equal. f_equal.
apply map_ext_in. intros. apply H3; auto.
- rewrite H3; trivial. now rewrite (rem_equiv a (FN n') H1).
Qed.
Lemma FN_equiv_shift p' a :
Perm p -> Inv p' p -> a el FN (p *' n) <-> p' a el FN n.
Proof.
intros H1 H2. split; intros H4.
- rewrite FN_equiv in H4; try assumption. now rewrite <-(perm_list_shift (FN n) a H2).
- rewrite FN_equiv; try assumption. now rewrite (perm_list_shift (FN n) a H2).
Qed.
Lemma no_nusk_equiv k :
Perm p -> NoNusk k n -> NoNusk k (p *' n).
Proof.
intros HP H1. rewrite <-BN_no_nusk in H1; trivial. apply BN_no_nusk; auto using nt_perm_wr.
intros a. rewrite <-BN_equiv.
destruct HP as [HP1 [p' HP2]].
rewrite (perm_list_shift (BN n) a (inv_comm HP2)).
intros H2 H3. apply (H1 (p' a)); trivial. rewrite HP1.
destruct (HP2 a) as [_ HP3]. now rewrite HP3.
Qed.
End Equivariance.
Hint Resolve ntwrA ntwrB nt_wr_sub nt_wr_sub' tree_wr_sub inv_comm nt_perm_wr free_sub_not list_max_max nth_In.
(*
Later we often need a fresh name relative to these parameters
*)
Definition fresh A n t k :=
fresh' (A ++ nt_names n ++ names t) k.
Lemma freshness A n t k :
let x := fresh A n t k in
~x el A /\ ~x el nt_names n /\ ~x el names t /\ k = rk x.
Proof.
intros x.
assert(H1: ~x el (A++(nt_names n)++(names t))) by apply freshness'.
rewrite in_app_iff, in_app_iff in H1. intuition.
Qed.
Lemma fresh_name A n t k :
{ x | ~x el A /\ ~x el nt_names n /\ ~x el names t /\ k = rk x}.
Proof.
pose(f:= fresh A n t k). exists f. apply freshness.
Qed.
Inductive NtAccept : list Name -> NuTree -> Tree -> Prop :=
| DNLs A l l' a :
(|l| = |l'|) ->
(forall (k : nat), k < |l| -> NtAccept (a::A) (nth k l DNT) (nth k l' DTR)) ->
NtAccept A (Tr a l) (TrA a l')
| DNNu A n t a b :
~ b el A -> ~ b el FN (Nu a n) -> rk a = rk b ->
NtAccept (b::A) (a$b *' n) t ->
NtAccept A (Nu a n) t.
Notation "t 'El' [ n ] A" := (NtAccept A n t)(at level 80).
(*
Top node name has to match
*)
Lemma ntl_name A a a' l l':
TrA a' l' El [ Tr a l] A -> a = a'.
Proof. now inversion 1. Qed.
(*
If a name c appears as a free name in a nu-tree n, and t is in
the language of n, then the name c has to be in t.
Intuitively, a free name is not permuted or instantiated.
*)
Lemma ntl_name_in n t c :
Ntwr n -> forall A, t El [n] A -> c el FN n -> c el names t.
Proof.
intros H2 A H3 HC.
induction H3 as [A l l' a H3 H4 H5| A n t a b H3 H4 H5 H6 H7]; simpl in *.
- destruct HC as [|[lc [H6 H7]] % concat_el]; try now left.
rewrite nth_el_indx_map with (x:= DNT) in H7. destruct H7 as [k [H7 H8]].
right. apply concat_map_el. subst lc.
exists (nth k l' DTR). split.
+ apply nth_In. congruence.
+ apply H5; try assumption. solve_wr_sub.
- inversion H2. apply in_rem_iff in HC as [HC1 HC2]. rewrite in_rem_iff in H4.
apply H7; auto. rewrite FN_equiv_shift with (p':=a$b); auto. solve_dec; tauto.
Qed.
Lemma ntl_name_not_in n t c :
Ntwr n -> forall A, t El [n] A -> ~c el names t -> ~c el FN n.
Proof.
intros H2 A H3 HA HC.
induction H3 as [A l l' a H3 H4 H5| A n t a b H3 H4 H5 H6 H7]; simpl in *.
- intuition. apply concat_el in H as [nl [H6 H7]].
rewrite nth_el_indx_map with (x:=DNT) in H7. destruct H7 as [k [H7 H8]]. subst nl.
apply (H5 k); auto; try solve_wr_sub; try congruence; try intros [|]; auto. intros H8.
apply H1, concat_map_el. exists (nth k l' DTR). split; trivial. apply nth_In. congruence.
- inversion H2. subst. rewrite in_rem_iff in H4.
rewrite in_rem_iff in HC. destruct HC as [H8 H9].
apply H7; auto. rewrite FN_equiv_shift with (p':=a$b); auto.
solve_dec; tauto.
Qed.
(*
Order of names doesn't matter in the list of names that have been seen before.
*)
Lemma ntl_swap_list A B n t :
t El [n] A -> A === B -> t El [n] B.
Proof.
intros HD. revert B.
induction HD as [A l l' a H1 _ H3| A n t a b H1 H2 H3 _ H5]; intros B AB.
- constructor; trivial. intros k KL.
apply H3; trivial. now rewrite AB.
- econstructor; try eassumption.
+ rewrite <- AB. apply H1.
+ apply H5. now rewrite AB.
Qed.
(*
Equivariance of the nu-tree language
*)
Fact ntl_equiv' n t A p :
Perm p -> Ntwr n -> t El [n] A -> p *> t El [p *' n] p *- A.
Proof.
intros HP HW H1. induction H1 as [A' l l' a'' H3 H4 H5| A' n t a b H3 H4 H5 H6 H7].
- simpl. constructor.
+ now rewrite map_length, map_length.
+ intros k H8. rewrite map_length in H8.
rewrite nth_indep with (d' := p *' DNT), nth_indep with (d' := p *> DTR); solve_len.
rewrite map_nth, map_nth. apply H5; auto. solve_wr_sub.
- apply DNNu with (b := p b); fold nt_apply_perm; auto.
+ now intros H8 % perm_list_el.
+ simpl in *. rewrite FN_equiv, <-rem_equiv, perm_list_el; auto; solve_wr_sub.
+ rewrite <-nt_assoc in H7; eauto.
rewrite <-perm_list_step, <-nt_assoc,
nt_swap_perm with (p':=p**a$b); try solve_wr_sub; eauto.
symmetry. now apply transp_compose.
Qed.
(*
This fact is shown using the previous fact and the permutation inverse.
*)
Fact ntl_equiv'' n t A p :
Twr t -> Perm p -> Ntwr n -> p *> t El [p *' n] p *- A -> t El [n] A.
Proof.
intros HT HP. assert(H2: Perm p) by assumption.
destruct HP as [_ [p' HP]]. intros HW H1. assert(HP2: Inv p' p) by apply inv_comm, HP.
apply (ntl_equiv' (perm_inv_perm H2 HP) (nt_perm_wr HW H2)) in H1.
now rewrite <-(perm_apply_inv HT HP2), <-(nt_perm_apply_inv HW HP2), (perm_list_inv A (inv_comm HP)) in H1.
Qed.
Theorem ntl_equiv n t A p :
Twr t -> Perm p -> Ntwr n -> t El [n] A <-> p *> t El [p *' n] p *- A.
Proof.
intros HW1 HP HW2. split.
- intros. now apply ntl_equiv'.
- now intros H % ntl_equiv''.
Qed.
Section Structure.
(*
Deciding structural equality on wellranked nu-trees.
We consider nu-trees structurally equal if they only differ in the names
of bindings.
The free names and the rest of the strucutre have to be the same.
*)
Variable n : NuTree.
Variable n' : NuTree.
Hypothesis HW1 : Ntwr n.
Hypothesis HW2 : Ntwr n'.
Inductive NtStr : NuTree -> NuTree -> Prop :=
| NtStrA a l l' : |l| = |l'| -> |l| = rk a -> (forall k, k < |l| -> NtStr (nth k l DNT) (nth k l' DNT)) -> NtStr (Tr a l) (Tr a l')
| NtStrB a b n n' : rk a = rk b -> ~ b el FN(n') -> ~b el FN(n) -> NtStr n (a$b *' n') -> NtStr (Nu a n) (Nu b n').
Fixpoint nt_str n n' : bool :=
match n, n' with
| Tr a l, Tr b l' =>
if Dec (a=b)
then all_true (map_pw (map nt_str l) l')
else false
| Nu a m, Nu b m' =>
if Dec (rk a = rk b)
then if Dec(~ b el FN m')
then if Dec(~ b el FN m)
then nt_str m (a$b *' m')
else false
else false
else false
| _, _ => false
end.
Lemma rem_id (X: eqType) (x: X) (A : list X) :
~ x el A -> rem A x = A.
Proof.
intros D. apply filter_id. intros y E.
apply Dec_reflect. congruence.
Qed.
Fact nt_str_correct_1 :
NtStr n n' -> nt_str n n' = true.
Proof.
induction 1 as [a l l' H1 H2 H3 H4| a b n n' H1 H2 H3]; simpl.
- decide (a=a) as [_|]; auto. rewrite all_true_map_pw_map with (x:=DNT)(y:=DNT); auto.
intros k H5. apply (H4 k H5); solve_wr_sub.
- inversion HW1. inversion HW2. subst.
decide (rk a = rk b) as [_|]; auto.
decide (~ b el FN n') as [_|]; auto.
decide (~ b el FN n) as [_|]; auto.
Qed.
Fact nt_str_correct_2 :
nt_str n n' = true -> NtStr n n'.
Proof.
revert HW2. revert n'. induction HW1 as [a l H1 H2 H3| a n H1 H2]; intros n' HW2; induction HW2 as [b l' H4 H5 H6| b n' H4 H5]; simpl; try discriminate 1.
- decide (a=b) as [E|]; try discriminate 1. subst b. rewrite all_true_map_pw_map with (x:=DNT)(y:=DNT); try congruence.
intros H7. constructor; auto; try congruence. intros k H8. apply H2; auto. apply H4, nth_In. congruence.
- decide (rk a = rk b) as [E1|]; try discriminate 1.
decide (~ b el (FN n')) as [E2|]; try discriminate 1.
decide (~ b el (FN n)) as [E3|]; try discriminate 1.
intros H6. constructor; auto.
Qed.
Fact nt_str_correct :
nt_str n n' = true <-> NtStr n n'.
Proof.
intros; split; eauto using nt_str_correct_1, nt_str_correct_2.
Qed.
Fact nt_str_dec :
dec (NtStr n n').
Proof.
destruct (nt_str n n') eqn:E.
- left. apply nt_str_correct; assumption.
- right. intros H3. apply nt_str_correct in H3; try assumption. congruence.
Qed.
(*
Structurally similar nu-trees have the same free names
*)
Fact nt_str_FN :
NtStr n n' -> FN n = FN n'.
Proof.
induction 1.
- simpl. f_equal. rewrite map_eq with (l':=l')(x:=DNT); auto.
intros. apply H2; auto; solve_wr_sub.
- simpl. inversion HW1. inversion HW2. subst.
decide(a el (FN n')) as [E1|E1].
+ exfalso. apply H1.
rewrite IHNtStr, FN_equiv_shift with (p':=a$b); auto. solve_dec.
+ rewrite IHNtStr, FN_equiv, <-rem_equiv' with (a:=b); auto.
* rewrite transp_list_indep; auto.
* solve_dec.
Qed.
End Structure.