proposition: Lemma int_red_preserve_hd : forall u v, int_red R u v -> exists f us vs, u = Fun f us /\ v = Fun f vs.
proof: Proof. intros. do 5 destruct H. intuition. destruct x1. congruence. simpl in *. ex f (Vcast (Vapp t (Vcons (fill x1 (sub x2 x)) t0)) e) (Vcast (Vapp t (Vcons (fill x1 (sub x2 x0)) t0)) e). tauto. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)