proposition: Theorem hlist_hrel_app : forall l ls x xs y ys, @hlist_hrel A F G R (l ++ ls) (hlist_app x xs) (hlist_app y ys) -> @hlist_hrel A F G R l x y /\ @hlist_hrel A F G R ls xs ys.
proof: Proof. induction x. + intros xs y ys. rewrite (hlist_eta y). simpl; intros; split; auto. constructor. + intros xs y ys. rewrite (hlist_eta y). intros. eapply hlist_hrel_cons in H. destruct H. apply IHx in H0. intuition. constructor; auto. Qed.
imports: Coq.Lists.List Coq.Arith.PeanoNat Relations RelationClasses ExtLib.Core.RelDec ExtLib.Data.SigT ExtLib.Data.Member ExtLib.Data.ListNth ExtLib.Data.Option ExtLib.Tactics Coq.Classes.Morphisms