proposition: Theorem restrict_code_encode_incl : forall (m1 : list A) (c : code A), incl m1 m -> encode A_eq_dec c m1 = encode A_eq_dec (restrict_code m c) m1.
proof: Proof. intros m1 c; elim m1; simpl in |- *; auto. intros a l H H0. apply f_equal2 with (f := app (A:=bool)); auto with datatypes. apply restrict_code_in; auto with datatypes. apply H; apply incl_tran with (2 := H0); auto with datatypes. Qed.
imports: Coq(Sorting.Permutation)