{w : SymbolType σ} (a b : FamilyProd (A&&P) (dom_symboltype w)) (R : for_all_2_family_prod (A&&P) (A&&P) cong_trace a b) : for_all_2_family_prod A A Φ (map_family_prod i a) (map_family_prod i b). Proof with try assumption. induction w... destruct a as [x a], b as [y b], R as [C R]. split... apply IHw... Qed.
Require Import Import